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/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.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.: 52 77 518 2834
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.257883071899
Defining function dvb_usb_device_init as symbolic
Defining function printk as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'release_firmware' (function is undefined)
Defining function request_firmware as symbolic
Defining function mutex_lock_interruptible_nested as symbolic
Defining function usb_control_msg as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Removed calls to 'dvb_usb_device_exit' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function usb_register_driver as symbolic
Defining function ldv_probe_1 as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function pskb_expand_head as symbolic
Defining function skb_clone as symbolic
Defining function skb_copy as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  __memcpy
  kfree
  __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.229593038559
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 94 79 338 1687
INFO: Starting verification
KLEE: WARNING: undefined reference to function: dvb_usb_device_exit
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_c6e6edff-fd92-4200-ac1e-81d740b8c96a/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:6890: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7206: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7206: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7353: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7821: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8089: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7812: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8106: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8029: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7841: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7792: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8051: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7856: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8119: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8073: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8090: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8107: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7870: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8074: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8035: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8121: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7776: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8058: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14483 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7873: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14978 states (over memory cap)
KLEE: WARNING: killing 15035 states (over memory cap)
KLEE: WARNING: killing 15096 states (over memory cap)
KLEE: WARNING: killing 14884 states (over memory cap)
KLEE: WARNING: killing 14813 states (over memory cap)
KLEE: WARNING: killing 14205 states (over memory cap)
KLEE: WARNING: killing 14420 states (over memory cap)
KLEE: WARNING: killing 15054 states (over memory cap)
KLEE: WARNING: killing 14594 states (over memory cap)
KLEE: WARNING: killing 14815 states (over memory cap)
KLEE: WARNING: killing 15040 states (over memory cap)
KLEE: WARNING: killing 14454 states (over memory cap)
KLEE: WARNING: killing 14818 states (over memory cap)
KLEE: WARNING: killing 15849 states (over memory cap)
KLEE: WARNING: killing 14717 states (over memory cap)
KLEE: WARNING: killing 15471 states (over memory cap)
KLEE: WARNING: killing 15290 states (over memory cap)
KLEE: WARNING: killing 14718 states (over memory cap)
KLEE: WARNING: killing 15329 states (over memory cap)
KLEE: WARNING: killing 15409 states (over memory cap)
KLEE: WARNING: killing 15222 states (over memory cap)
KLEE: WARNING: killing 15176 states (over memory cap)
KLEE: WARNING: killing 15125 states (over memory cap)
KLEE: WARNING: killing 15469 states (over memory cap)
KLEE: WARNING: killing 15288 states (over memory cap)
KLEE: WARNING: killing 15762 states (over memory cap)
KLEE: WARNING: killing 15459 states (over memory cap)
KLEE: WARNING: killing 15291 states (over memory cap)
KLEE: WARNING: killing 15631 states (over memory cap)
KLEE: WARNING: killing 15464 states (over memory cap)
KLEE: WARNING: killing 14904 states (over memory cap)
KLEE: WARNING: killing 15247 states (over memory cap)
KLEE: WARNING: killing 15204 states (over memory cap)
KLEE: WARNING: killing 15670 states (over memory cap)
KLEE: WARNING: killing 15492 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7856: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15314 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8107: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15403 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8074: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15497 states (over memory cap)
KLEE: WARNING: killing 15828 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7821: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15027 states (over memory cap)
KLEE: WARNING: killing 15601 states (over memory cap)
KLEE: WARNING: killing 15177 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8090: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14755 states (over memory cap)
KLEE: WARNING: killing 15459 states (over memory cap)
KLEE: WARNING: killing 15041 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7830: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15000 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8106: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15206 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8089: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15776 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7792: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7812: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8403: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:7841: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15730 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-dHiDKj/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--usb--dvb-usb--dvb-usb-gp8psk.ko-entry_point_true-unreach-call.cil.out.c:8073: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15695 states (over memory cap)
KLEE: WARNING: killing 15524 states (over memory cap)
KLEE: WARNING: killing 15597 states (over memory cap)
KLEE: WARNING: killing 15192 states (over memory cap)
KLEE: WARNING: killing 15396 states (over memory cap)
KLEE: WARNING: killing 15229 states (over memory cap)
KLEE: WARNING: killing 15307 states (over memory cap)
KLEE: WARNING: killing 15635 states (over memory cap)
KLEE: WARNING: killing 15825 states (over memory cap)
KLEE: WARNING: killing 15549 states (over memory cap)
KLEE: WARNING: killing 15389 states (over memory cap)
KLEE: WARNING: killing 15470 states (over memory cap)
KLEE: WARNING: killing 15655 states (over memory cap)
KLEE: WARNING: killing 15258 states (over memory cap)
KLEE: WARNING: killing 15456 states (over memory cap)
KLEE: WARNING: killing 15529 states (over memory cap)
KLEE: WARNING: killing 15617 states (over memory cap)
KLEE: WARNING: killing 15459 states (over memory cap)
KLEE: WARNING: killing 15409 states (over memory cap)
KLEE: WARNING: killing 15609 states (over memory cap)
KLEE: WARNING: killing 15565 states (over memory cap)
KLEE: WARNING: killing 15625 states (over memory cap)
KLEE: WARNING: killing 15590 states (over memory cap)
KLEE: WARNING: killing 15321 states (over memory cap)
KLEE: WARNING: killing 15401 states (over memory cap)
KLEE: WARNING: killing 15360 states (over memory cap)
KLEE: WARNING: killing 15773 states (over memory cap)
KLEE: WARNING: killing 15730 states (over memory cap)
KLEE: WARNING: killing 11519 states (over memory cap)
KLEE: WARNING: killing 14870 states (over memory cap)
KLEE: WARNING: killing 15510 states (over memory cap)
KLEE: WARNING: killing 11220 states (over memory cap)
KLEE: WARNING: killing 15111 states (over memory cap)
KLEE: WARNING: killing 15516 states (over memory cap)
KLEE: WARNING: killing 11143 states (over memory cap)
KLEE: WARNING: killing 15010 states (over memory cap)
KLEE: WARNING: killing 11205 states (over memory cap)
KLEE: WARNING: killing 14829 states (over memory cap)
KLEE: WARNING: killing 11373 states (over memory cap)
KLEE: WARNING: killing 14878 states (over memory cap)
