bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_x25.ko-entry_point_true-unreach-call.cil.out.c


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 17 63 289 1441
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.153563976288
Removed calls to 'linkwatch_fire_event' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Defining function skb_pull as symbolic
Defining function lapb_data_request as symbolic
Defining function lapb_connect_request as symbolic
Defining function netdev_err as symbolic
Defining function lapb_disconnect_request as symbolic
Defining function skb_put as symbolic
Defining function lapb_data_received as symbolic
Defining function skb_clone as symbolic
Defining function capable as symbolic
Defining function attach_hdlc_protocol as symbolic
Defining function lapb_unregister as symbolic
Defining function lapb_register as symbolic
Defining function skb_push as symbolic
Defining function pskb_expand_head as symbolic
Removed calls to 'unregister_hdlc_protocol' (function is undefined)
Removed calls to 'register_hdlc_protocol' (function is undefined)
Linked our definitions to these undefined functions:
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.194006919861
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 54 63 163 838
INFO: Starting verification
KLEE: WARNING ONCE: function "x25_ioctl" has inline asm
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_46f9dfac-1852-4ab8-8389-7a99cc3ce902/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bZ9zV_/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_x25.ko-entry_point_true-unreach-call.cil.out.c:5598: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bZ9zV_/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_x25.ko-entry_point_true-unreach-call.cil.out.c:5518: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bZ9zV_/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_x25.ko-entry_point_true-unreach-call.cil.out.c:5632: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bZ9zV_/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_x25.ko-entry_point_true-unreach-call.cil.out.c:5518: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bZ9zV_/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_x25.ko-entry_point_true-unreach-call.cil.out.c:5601: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bZ9zV_/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_x25.ko-entry_point_true-unreach-call.cil.out.c:5612: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 14670 states (over memory cap)
KLEE: WARNING: killing 13460 states (over memory cap)
KLEE: WARNING: killing 13242 states (over memory cap)
KLEE: WARNING: killing 13515 states (over memory cap)
KLEE: WARNING: killing 13917 states (over memory cap)
KLEE: WARNING: killing 13710 states (over memory cap)
KLEE: WARNING: killing 13752 states (over memory cap)
KLEE: WARNING: killing 13802 states (over memory cap)
KLEE: WARNING: killing 14077 states (over memory cap)
KLEE: WARNING: killing 13895 states (over memory cap)
KLEE: WARNING: killing 13939 states (over memory cap)
KLEE: WARNING: killing 13762 states (over memory cap)
KLEE: WARNING: killing 13691 states (over memory cap)
KLEE: WARNING: killing 13977 states (over memory cap)
KLEE: WARNING: killing 13681 states (over memory cap)
KLEE: WARNING: killing 13844 states (over memory cap)
KLEE: WARNING: killing 13663 states (over memory cap)
KLEE: WARNING: killing 13494 states (over memory cap)
KLEE: WARNING: killing 14106 states (over memory cap)
KLEE: WARNING: killing 13701 states (over memory cap)
KLEE: WARNING: killing 14099 states (over memory cap)
KLEE: WARNING: killing 11287 states (over memory cap)
KLEE: WARNING: killing 13995 states (over memory cap)
KLEE: WARNING: killing 13937 states (over memory cap)
KLEE: WARNING: killing 11046 states (over memory cap)
KLEE: WARNING: killing 13395 states (over memory cap)
KLEE: WARNING: killing 11183 states (over memory cap)
KLEE: WARNING: killing 13742 states (over memory cap)
KLEE: WARNING: killing 10991 states (over memory cap)
KLEE: WARNING: killing 13635 states (over memory cap)
KLEE: WARNING: killing 11347 states (over memory cap)
KLEE: WARNING: killing 10992 states (over memory cap)
KLEE: WARNING: killing 10638 states (over memory cap)
KLEE: WARNING: killing 10607 states (over memory cap)
KLEE: WARNING: killing 13325 states (over memory cap)
KLEE: WARNING: killing 10750 states (over memory cap)
KLEE: WARNING: killing 10610 states (over memory cap)
KLEE: WARNING: killing 10785 states (over memory cap)
KLEE: WARNING: killing 10755 states (over memory cap)
KLEE: WARNING: killing 10513 states (over memory cap)
KLEE: WARNING: killing 10581 states (over memory cap)
KLEE: WARNING: killing 10759 states (over memory cap)
KLEE: WARNING: killing 10729 states (over memory cap)
KLEE: WARNING: killing 11115 states (over memory cap)
KLEE: WARNING: killing 10466 states (over memory cap)
KLEE: WARNING: killing 10948 states (over memory cap)
KLEE: WARNING: killing 10614 states (over memory cap)
KLEE: WARNING: killing 10482 states (over memory cap)
KLEE: WARNING: killing 10757 states (over memory cap)
KLEE: WARNING: killing 10631 states (over memory cap)
KLEE: WARNING: killing 10696 states (over memory cap)
KLEE: WARNING: killing 10673 states (over memory cap)
KLEE: WARNING: killing 10740 states (over memory cap)
KLEE: WARNING: killing 10915 states (over memory cap)
KLEE: WARNING: killing 10886 states (over memory cap)
KLEE: WARNING: killing 10852 states (over memory cap)
KLEE: WARNING: killing 10722 states (over memory cap)
