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--ieee802154--mrf24j40.ko-entry_point_false-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.: 94 82 594 4188
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.24872803688
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'ieee802154_unregister_device' (function is undefined)
Removed calls to 'ieee802154_free_device' (function is undefined)
Defining function printk as symbolic
Defining function ieee802154_alloc_device as symbolic
Defining function ieee802154_register_device as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'complete' (function is undefined)
Removed calls to 'skb_trim' (function is undefined)
Removed calls to 'ieee802154_rx_irqsafe' (function is undefined)
Defining function dev_err as symbolic
Defining function devm_request_threaded_irq as symbolic
Defining function skb_put as symbolic
Defining function devm_kmalloc as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function wait_for_completion_interruptible_timeout as symbolic
Defining function dev_warn as symbolic
Defining function ldv_handler1_2 as symbolic
Defining function ldv_handler1_1 as symbolic
Removed calls to 'driver_unregister' (function is undefined)
Defining function spi_register_driver as symbolic
Linked our definitions to these undefined functions:
  __memcpy
  __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.262998104095
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 147 77 316 2583
INFO: Starting verification
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_6563836b-c049-4f06-b6d7-139364648a61/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:6219: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:6232: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:6306: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:6124: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:6610: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:6387: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:5870: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:5782: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:6139: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:6619: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:6619: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:6402: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:6427: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:6446: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:5739: 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 14121 states (over memory cap)
KLEE: WARNING: killing 14060 states (over memory cap)
KLEE: WARNING: killing 13302 states (over memory cap)
KLEE: WARNING: killing 13821 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:5404: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13196 states (over memory cap)
KLEE: WARNING: killing 13715 states (over memory cap)
KLEE: WARNING: killing 13438 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:5918: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13847 states (over memory cap)
KLEE: WARNING: killing 13566 states (over memory cap)
KLEE: WARNING: killing 14089 states (over memory cap)
KLEE: WARNING: killing 14047 states (over memory cap)
KLEE: WARNING: killing 13885 states (over memory cap)
KLEE: WARNING: killing 13843 states (over memory cap)
KLEE: WARNING: killing 14253 states (over memory cap)
KLEE: WARNING: killing 14214 states (over memory cap)
KLEE: WARNING: killing 14283 states (over memory cap)
KLEE: WARNING: killing 13798 states (over memory cap)
KLEE: WARNING: killing 14315 states (over memory cap)
KLEE: WARNING: killing 14066 states (over memory cap)
KLEE: WARNING: killing 14692 states (over memory cap)
KLEE: WARNING: killing 14209 states (over memory cap)
KLEE: WARNING: killing 14285 states (over memory cap)
KLEE: WARNING: killing 14463 states (over memory cap)
KLEE: WARNING: killing 13987 states (over memory cap)
KLEE: WARNING: killing 14385 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-L4Qfml/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ieee802154--mrf24j40.ko-entry_point_false-unreach-call.cil.out.c:6633: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13911 states (over memory cap)
KLEE: WARNING: killing 14089 states (over memory cap)
KLEE: WARNING: killing 13948 states (over memory cap)
KLEE: WARNING: killing 13910 states (over memory cap)
KLEE: WARNING: killing 14095 states (over memory cap)
KLEE: WARNING: killing 13737 states (over memory cap)
KLEE: WARNING: killing 13600 states (over memory cap)
KLEE: WARNING: killing 13773 states (over memory cap)
KLEE: WARNING: killing 13955 states (over memory cap)
KLEE: WARNING: killing 14244 states (over memory cap)
KLEE: WARNING: killing 13890 states (over memory cap)
KLEE: WARNING: killing 13962 states (over memory cap)
KLEE: WARNING: killing 13828 states (over memory cap)
KLEE: WARNING: killing 13368 states (over memory cap)
KLEE: WARNING: killing 14071 states (over memory cap)
KLEE: WARNING: killing 14247 states (over memory cap)
KLEE: WARNING: killing 14326 states (over memory cap)
KLEE: WARNING: killing 14090 states (over memory cap)
KLEE: WARNING: killing 13946 states (over memory cap)
KLEE: WARNING: killing 13813 states (over memory cap)
KLEE: WARNING: killing 14306 states (over memory cap)
KLEE: WARNING: killing 14378 states (over memory cap)
KLEE: WARNING: killing 13834 states (over memory cap)
KLEE: WARNING: killing 13904 states (over memory cap)
KLEE: WARNING: killing 13668 states (over memory cap)
KLEE: WARNING: killing 13845 states (over memory cap)
KLEE: WARNING: killing 14431 states (over memory cap)
KLEE: WARNING: killing 14093 states (over memory cap)
KLEE: WARNING: killing 14274 states (over memory cap)
KLEE: WARNING: killing 13944 states (over memory cap)
KLEE: WARNING: killing 13910 states (over memory cap)
KLEE: WARNING: killing 13784 states (over memory cap)
KLEE: WARNING: killing 13752 states (over memory cap)
KLEE: WARNING: killing 13922 states (over memory cap)
KLEE: WARNING: killing 13893 states (over memory cap)
KLEE: WARNING: killing 13964 states (over memory cap)
KLEE: WARNING: killing 14135 states (over memory cap)
KLEE: WARNING: killing 13803 states (over memory cap)
KLEE: WARNING: killing 14172 states (over memory cap)
KLEE: WARNING: killing 13953 states (over memory cap)
KLEE: WARNING: killing 13825 states (over memory cap)
KLEE: WARNING: killing 14194 states (over memory cap)
KLEE: WARNING: killing 13772 states (over memory cap)
KLEE: WARNING: killing 14046 states (over memory cap)
KLEE: WARNING: killing 13819 states (over memory cap)
KLEE: WARNING: killing 13890 states (over memory cap)
KLEE: WARNING: killing 14258 states (over memory cap)
KLEE: WARNING: killing 14138 states (over memory cap)
KLEE: WARNING: killing 14012 states (over memory cap)
KLEE: WARNING: killing 13983 states (over memory cap)
KLEE: WARNING: killing 13858 states (over memory cap)
KLEE: WARNING: killing 13930 states (over memory cap)
KLEE: WARNING: killing 14006 states (over memory cap)
KLEE: WARNING: killing 14180 states (over memory cap)
KLEE: WARNING: killing 13958 states (over memory cap)
KLEE: WARNING: killing 13939 states (over memory cap)
KLEE: WARNING: killing 13907 states (over memory cap)
KLEE: WARNING: killing 13790 states (over memory cap)
KLEE: WARNING: killing 13660 states (over memory cap)
KLEE: WARNING: killing 13836 states (over memory cap)
KLEE: WARNING: killing 14100 states (over memory cap)
KLEE: WARNING: killing 14266 states (over memory cap)
KLEE: WARNING: killing 13564 states (over memory cap)
KLEE: WARNING: killing 14019 states (over memory cap)
KLEE: WARNING: killing 14088 states (over memory cap)
KLEE: WARNING: killing 13778 states (over memory cap)
KLEE: WARNING: killing 13752 states (over memory cap)
KLEE: WARNING: killing 14010 states (over memory cap)
KLEE: WARNING: killing 13993 states (over memory cap)
KLEE: WARNING: killing 13772 states (over memory cap)
KLEE: WARNING: killing 13839 states (over memory cap)
KLEE: WARNING: killing 13905 states (over memory cap)
KLEE: WARNING: killing 13977 states (over memory cap)
KLEE: WARNING: killing 13953 states (over memory cap)
KLEE: WARNING: killing 13832 states (over memory cap)
KLEE: WARNING: killing 14000 states (over memory cap)
KLEE: WARNING: killing 13884 states (over memory cap)
KLEE: WARNING: killing 13951 states (over memory cap)
KLEE: WARNING: killing 14119 states (over memory cap)
KLEE: WARNING: killing 13909 states (over memory cap)
KLEE: WARNING: killing 13793 states (over memory cap)
KLEE: WARNING: killing 13859 states (over memory cap)
KLEE: WARNING: killing 13743 states (over memory cap)
KLEE: WARNING: killing 13714 states (over memory cap)
KLEE: WARNING: killing 13966 states (over memory cap)
KLEE: WARNING: killing 14134 states (over memory cap)
KLEE: WARNING: killing 13834 states (over memory cap)
KLEE: WARNING: killing 13995 states (over memory cap)
KLEE: WARNING: killing 13873 states (over memory cap)
KLEE: WARNING: killing 14039 states (over memory cap)
KLEE: WARNING: killing 13739 states (over memory cap)
KLEE: WARNING: killing 13807 states (over memory cap)
KLEE: WARNING: killing 13870 states (over memory cap)
KLEE: WARNING: killing 14218 states (over memory cap)
KLEE: WARNING: killing 14008 states (over memory cap)
KLEE: WARNING: killing 13892 states (over memory cap)
KLEE: WARNING: killing 13962 states (over memory cap)
KLEE: WARNING: killing 14125 states (over memory cap)
KLEE: WARNING: killing 14100 states (over memory cap)
KLEE: WARNING: killing 13895 states (over memory cap)
KLEE: WARNING: killing 13688 states (over memory cap)
