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_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--cdc_eem.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.: 30 67 335 1790
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.190931081772
Defining function usbnet_probe as symbolic
Defining function usbnet_suspend as symbolic
Defining function usbnet_resume as symbolic
Removed calls to 'usb_driver_release_interface' (function is undefined)
Removed calls to 'skb_trim' (function is undefined)
Removed calls to 'usb_free_urb' (function is undefined)
Removed calls to 'usbnet_device_suggests_idle' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to 'usbnet_skb_return' (function is undefined)
Defining function skb_copy_expand as symbolic
Defining function crc32_le as symbolic
Defining function skb_put as symbolic
Defining function skb_push as symbolic
Defining function skb_pull as symbolic
Defining function skb_clone as symbolic
Defining function netdev_warn as symbolic
Defining function usb_alloc_urb as symbolic
Defining function usb_submit_urb as symbolic
Defining function usbnet_get_endpoints as symbolic
Removed calls to 'usbnet_disconnect' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Defining function ldv_reset_resume_1 as symbolic
Defining function ldv_release_2 as symbolic
Defining function usb_register_driver as symbolic
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.240561962128
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 73 60 190 1017
INFO: Starting verification
KLEE: WARNING: undefined reference to function: usbnet_disconnect
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_5e7cf9b0-da0f-4588-b987-2c6f91b47a5b/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pTAKJl/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--cdc_eem.ko-entry_point_true-unreach-call.cil.out.c:5937: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pTAKJl/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--cdc_eem.ko-entry_point_true-unreach-call.cil.out.c:5914: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pTAKJl/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--cdc_eem.ko-entry_point_true-unreach-call.cil.out.c:6013: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pTAKJl/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--cdc_eem.ko-entry_point_true-unreach-call.cil.out.c:5940: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pTAKJl/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--cdc_eem.ko-entry_point_true-unreach-call.cil.out.c:5914: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pTAKJl/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--cdc_eem.ko-entry_point_true-unreach-call.cil.out.c:5940: divide by zero
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 14002 states (over memory cap)
KLEE: WARNING: killing 12810 states (over memory cap)
KLEE: WARNING: killing 12733 states (over memory cap)
KLEE: WARNING: killing 12779 states (over memory cap)
KLEE: WARNING: killing 12827 states (over memory cap)
KLEE: WARNING: killing 13123 states (over memory cap)
KLEE: WARNING: killing 13532 states (over memory cap)
KLEE: WARNING: killing 13231 states (over memory cap)
KLEE: WARNING: killing 13524 states (over memory cap)
KLEE: WARNING: killing 13467 states (over memory cap)
KLEE: WARNING: killing 13644 states (over memory cap)
KLEE: WARNING: killing 13821 states (over memory cap)
KLEE: WARNING: killing 13884 states (over memory cap)
KLEE: WARNING: killing 13951 states (over memory cap)
KLEE: WARNING: killing 14127 states (over memory cap)
KLEE: WARNING: killing 13967 states (over memory cap)
KLEE: WARNING: killing 14492 states (over memory cap)
KLEE: WARNING: killing 14665 states (over memory cap)
KLEE: WARNING: killing 14498 states (over memory cap)
KLEE: WARNING: killing 14217 states (over memory cap)
KLEE: WARNING: killing 14395 states (over memory cap)
KLEE: WARNING: killing 14352 states (over memory cap)
KLEE: WARNING: killing 14751 states (over memory cap)
KLEE: WARNING: killing 14700 states (over memory cap)
KLEE: WARNING: killing 14412 states (over memory cap)
KLEE: WARNING: killing 14928 states (over memory cap)
KLEE: WARNING: killing 14879 states (over memory cap)
KLEE: WARNING: killing 15057 states (over memory cap)
KLEE: WARNING: killing 14894 states (over memory cap)
KLEE: WARNING: killing 15283 states (over memory cap)
KLEE: WARNING: killing 15129 states (over memory cap)
KLEE: WARNING: killing 15302 states (over memory cap)
KLEE: WARNING: killing 14815 states (over memory cap)
KLEE: WARNING: killing 14979 states (over memory cap)
KLEE: WARNING: killing 15036 states (over memory cap)
KLEE: WARNING: killing 10796 states (over memory cap)
KLEE: WARNING: killing 14522 states (over memory cap)
KLEE: WARNING: killing 14900 states (over memory cap)
KLEE: WARNING: killing 15068 states (over memory cap)
KLEE: WARNING: killing 10775 states (over memory cap)
KLEE: WARNING: killing 14990 states (over memory cap)
KLEE: WARNING: killing 10613 states (over memory cap)
KLEE: WARNING: killing 14705 states (over memory cap)
KLEE: WARNING: killing 10559 states (over memory cap)
KLEE: WARNING: killing 14416 states (over memory cap)
KLEE: WARNING: killing 10816 states (over memory cap)
KLEE: WARNING: killing 14976 states (over memory cap)
KLEE: WARNING: killing 10869 states (over memory cap)
KLEE: WARNING: killing 14789 states (over memory cap)
KLEE: WARNING: killing 10708 states (over memory cap)
KLEE: WARNING: killing 14405 states (over memory cap)
KLEE: WARNING: killing 10647 states (over memory cap)
KLEE: WARNING: killing 10631 states (over memory cap)
KLEE: WARNING: killing 10401 states (over memory cap)
KLEE: WARNING: killing 10483 states (over memory cap)
KLEE: WARNING: killing 14557 states (over memory cap)
KLEE: WARNING: killing 10733 states (over memory cap)
KLEE: WARNING: killing 10204 states (over memory cap)
KLEE: WARNING: killing 10390 states (over memory cap)
KLEE: WARNING: killing 14326 states (over memory cap)
KLEE: WARNING: killing 10951 states (over memory cap)
KLEE: WARNING: killing 10328 states (over memory cap)
KLEE: WARNING: killing 10209 states (over memory cap)
KLEE: WARNING: killing 10084 states (over memory cap)
KLEE: WARNING: killing 10171 states (over memory cap)
KLEE: WARNING: killing 10250 states (over memory cap)
KLEE: WARNING: killing 10328 states (over memory cap)
KLEE: WARNING: killing 10211 states (over memory cap)
KLEE: WARNING: killing 10395 states (over memory cap)
KLEE: WARNING: killing 10177 states (over memory cap)
KLEE: WARNING: killing 10359 states (over memory cap)
KLEE: WARNING: killing 10339 states (over memory cap)
KLEE: WARNING: killing 10121 states (over memory cap)
KLEE: WARNING: killing 10306 states (over memory cap)
KLEE: WARNING: killing 10089 states (over memory cap)
KLEE: WARNING: killing 10268 states (over memory cap)
KLEE: WARNING: killing 10452 states (over memory cap)
KLEE: WARNING: killing 10234 states (over memory cap)
KLEE: WARNING: killing 10315 states (over memory cap)
KLEE: WARNING: killing 10196 states (over memory cap)
KLEE: WARNING: killing 10368 states (over memory cap)
KLEE: WARNING: killing 10249 states (over memory cap)
KLEE: WARNING: killing 10527 states (over memory cap)
