bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--media--usb--dvb-usb-v2--dvb-usb-lmedm04.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.: 128 150 1053 7118
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.371220111847
Defining function dvb_usbv2_probe as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to '__symbol_put' (function is undefined)
Removed calls to 'dvb_frontend_detach' (function is undefined)
Removed calls to 'usb_kill_urb' (function is undefined)
Removed calls to 'usb_free_coherent' (function is undefined)
Defining function printk as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function usb_bulk_msg as symbolic
Defining function mutex_lock_interruptible as symbolic
Defining function __symbol_get as symbolic
Defining function __request_module as symbolic
Defining function usb_alloc_urb as symbolic
Defining function usb_alloc_coherent as symbolic
Removed calls to 'rc_keydown' (function is undefined)
Defining function usb_submit_urb as symbolic
Defining function __msecs_to_jiffies as symbolic
Removed calls to 'release_firmware' (function is undefined)
Defining function strlcpy as symbolic
Defining function strlcat as symbolic
Defining function request_firmware as symbolic
Defining function usb_reset_configuration as symbolic
Defining function usb_set_interface as symbolic
Defining function usb_control_msg as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'dvb_usbv2_disconnect' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Defining function usb_register_driver as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  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.322454929352
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 176 156 683 3577
INFO: Starting verification
KLEE: WARNING: undefined reference to function: dvb_usbv2_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_8e8d9c64-9a93-40f0-98f9-1e1c1c140851/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vY2BrL/linux-4.2-rc1.tar.xz-32_7a-drivers--media--usb--dvb-usb-v2--dvb-usb-lmedm04.ko-entry_point_true-unreach-call.cil.out.c:9430: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vY2BrL/linux-4.2-rc1.tar.xz-32_7a-drivers--media--usb--dvb-usb-v2--dvb-usb-lmedm04.ko-entry_point_true-unreach-call.cil.out.c:9371: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vY2BrL/linux-4.2-rc1.tar.xz-32_7a-drivers--media--usb--dvb-usb-v2--dvb-usb-lmedm04.ko-entry_point_true-unreach-call.cil.out.c:8134: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vY2BrL/linux-4.2-rc1.tar.xz-32_7a-drivers--media--usb--dvb-usb-v2--dvb-usb-lmedm04.ko-entry_point_true-unreach-call.cil.out.c:9336: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vY2BrL/linux-4.2-rc1.tar.xz-32_7a-drivers--media--usb--dvb-usb-v2--dvb-usb-lmedm04.ko-entry_point_true-unreach-call.cil.out.c:9184: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vY2BrL/linux-4.2-rc1.tar.xz-32_7a-drivers--media--usb--dvb-usb-v2--dvb-usb-lmedm04.ko-entry_point_true-unreach-call.cil.out.c:8903: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vY2BrL/linux-4.2-rc1.tar.xz-32_7a-drivers--media--usb--dvb-usb-v2--dvb-usb-lmedm04.ko-entry_point_true-unreach-call.cil.out.c:8242: 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 13373 states (over memory cap)
KLEE: WARNING: killing 15602 states (over memory cap)
KLEE: WARNING: killing 15293 states (over memory cap)
KLEE: WARNING: killing 15831 states (over memory cap)
KLEE: WARNING: killing 15766 states (over memory cap)
KLEE: WARNING: killing 15822 states (over memory cap)
KLEE: WARNING: killing 15526 states (over memory cap)
KLEE: WARNING: killing 15230 states (over memory cap)
KLEE: WARNING: killing 15992 states (over memory cap)
KLEE: WARNING: killing 15825 states (over memory cap)
KLEE: WARNING: killing 15538 states (over memory cap)
KLEE: WARNING: killing 16183 states (over memory cap)
KLEE: WARNING: killing 16836 states (over memory cap)
KLEE: WARNING: killing 16670 states (over memory cap)
KLEE: WARNING: killing 16737 states (over memory cap)
KLEE: WARNING: killing 16692 states (over memory cap)
KLEE: WARNING: killing 16529 states (over memory cap)
KLEE: WARNING: killing 16603 states (over memory cap)
KLEE: WARNING: killing 16780 states (over memory cap)
KLEE: WARNING: killing 16049 states (over memory cap)
KLEE: WARNING: killing 16240 states (over memory cap)
KLEE: WARNING: killing 16756 states (over memory cap)
KLEE: WARNING: killing 16371 states (over memory cap)
KLEE: WARNING: killing 16663 states (over memory cap)
KLEE: WARNING: killing 16955 states (over memory cap)
KLEE: WARNING: killing 16009 states (over memory cap)
KLEE: WARNING: killing 16525 states (over memory cap)
KLEE: WARNING: killing 16476 states (over memory cap)
KLEE: WARNING: killing 16437 states (over memory cap)
KLEE: WARNING: killing 16388 states (over memory cap)
KLEE: WARNING: killing 16455 states (over memory cap)
KLEE: WARNING: killing 16305 states (over memory cap)
KLEE: WARNING: killing 16697 states (over memory cap)
KLEE: WARNING: killing 16660 states (over memory cap)
KLEE: WARNING: killing 16178 states (over memory cap)
KLEE: WARNING: killing 16677 states (over memory cap)
KLEE: WARNING: killing 16640 states (over memory cap)
KLEE: WARNING: killing 16266 states (over memory cap)
KLEE: WARNING: killing 16662 states (over memory cap)
KLEE: WARNING: killing 16844 states (over memory cap)
KLEE: WARNING: killing 16701 states (over memory cap)
KLEE: WARNING: killing 16874 states (over memory cap)
KLEE: WARNING: killing 16410 states (over memory cap)
KLEE: WARNING: killing 16362 states (over memory cap)
KLEE: WARNING: killing 16972 states (over memory cap)
KLEE: WARNING: killing 16719 states (over memory cap)
KLEE: WARNING: killing 16364 states (over memory cap)
KLEE: WARNING: killing 16427 states (over memory cap)
KLEE: WARNING: killing 16926 states (over memory cap)
KLEE: WARNING: killing 16469 states (over memory cap)
KLEE: WARNING: killing 16431 states (over memory cap)
KLEE: WARNING: killing 16501 states (over memory cap)
KLEE: WARNING: killing 16361 states (over memory cap)
KLEE: WARNING: killing 16852 states (over memory cap)
KLEE: WARNING: killing 16917 states (over memory cap)
KLEE: WARNING: killing 16675 states (over memory cap)
KLEE: WARNING: killing 16747 states (over memory cap)
KLEE: WARNING: killing 16288 states (over memory cap)
KLEE: WARNING: killing 16470 states (over memory cap)
KLEE: WARNING: killing 16964 states (over memory cap)
KLEE: WARNING: killing 16925 states (over memory cap)
KLEE: WARNING: killing 16895 states (over memory cap)
KLEE: WARNING: killing 16748 states (over memory cap)
KLEE: WARNING: killing 16202 states (over memory cap)
KLEE: WARNING: killing 16479 states (over memory cap)
KLEE: WARNING: killing 15934 states (over memory cap)
KLEE: WARNING: killing 16519 states (over memory cap)
KLEE: WARNING: killing 16282 states (over memory cap)
KLEE: WARNING: killing 16964 states (over memory cap)
KLEE: WARNING: killing 16513 states (over memory cap)
KLEE: WARNING: killing 16688 states (over memory cap)
KLEE: WARNING: killing 17067 states (over memory cap)
KLEE: WARNING: killing 16421 states (over memory cap)
KLEE: WARNING: killing 16284 states (over memory cap)
KLEE: WARNING: killing 16556 states (over memory cap)
KLEE: WARNING: killing 16631 states (over memory cap)
KLEE: WARNING: killing 17103 states (over memory cap)
KLEE: WARNING: killing 16872 states (over memory cap)
KLEE: WARNING: killing 16340 states (over memory cap)
KLEE: WARNING: killing 16508 states (over memory cap)
KLEE: WARNING: killing 16773 states (over memory cap)
KLEE: WARNING: killing 16242 states (over memory cap)
KLEE: WARNING: killing 16614 states (over memory cap)
KLEE: WARNING: killing 16977 states (over memory cap)
KLEE: WARNING: killing 16348 states (over memory cap)
KLEE: WARNING: killing 16908 states (over memory cap)
KLEE: WARNING: killing 16183 states (over memory cap)
KLEE: WARNING: killing 16853 states (over memory cap)
KLEE: WARNING: killing 16420 states (over memory cap)
KLEE: WARNING: killing 16398 states (over memory cap)
KLEE: WARNING: killing 16763 states (over memory cap)
KLEE: WARNING: killing 16726 states (over memory cap)
KLEE: WARNING: killing 16594 states (over memory cap)
KLEE: WARNING: killing 16571 states (over memory cap)
KLEE: WARNING: killing 16543 states (over memory cap)
KLEE: WARNING: killing 16716 states (over memory cap)
KLEE: WARNING: killing 16575 states (over memory cap)
KLEE: WARNING: killing 16546 states (over memory cap)
KLEE: WARNING: killing 16415 states (over memory cap)
KLEE: WARNING: killing 16874 states (over memory cap)
KLEE: WARNING: killing 16452 states (over memory cap)
KLEE: WARNING: killing 16419 states (over memory cap)
KLEE: WARNING: killing 16488 states (over memory cap)
KLEE: WARNING: killing 16451 states (over memory cap)
KLEE: WARNING: killing 16522 states (over memory cap)
KLEE: WARNING: killing 16302 states (over memory cap)
KLEE: WARNING: killing 9558 states (over memory cap)
KLEE: WARNING: killing 15788 states (over memory cap)
KLEE: WARNING: killing 16512 states (over memory cap)
KLEE: WARNING: killing 16777 states (over memory cap)
KLEE: WARNING: killing 16648 states (over memory cap)
KLEE: WARNING: killing 16907 states (over memory cap)
KLEE: WARNING: killing 16309 states (over memory cap)
KLEE: WARNING: killing 16470 states (over memory cap)
KLEE: WARNING: killing 16439 states (over memory cap)
KLEE: WARNING: killing 9325 states (over memory cap)
KLEE: WARNING: killing 15370 states (over memory cap)
KLEE: WARNING: killing 9299 states (over memory cap)
KLEE: WARNING: killing 15506 states (over memory cap)
KLEE: WARNING: killing 16229 states (over memory cap)
KLEE: WARNING: killing 9532 states (over memory cap)
KLEE: WARNING: killing 15625 states (over memory cap)
KLEE: WARNING: killing 9320 states (over memory cap)
KLEE: WARNING: killing 15684 states (over memory cap)
KLEE: WARNING: killing 16022 states (over memory cap)
KLEE: WARNING: killing 9280 states (over memory cap)
