bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--b2c2--b2c2-flexcop-usb.ko-main.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.: 53 69 495 2774
Removed infinite loop in arch_local_save_flags
INFO: Compilation, preparation and instrumentation time: 0.197336196899
Removed calls to 'usb_deregister' (function is undefined)
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Removed calls to 'flexcop_wan_set_speed' (function is undefined)
Removed calls to 'flexcop_sram_ctrl' (function is undefined)
Removed calls to 'flexcop_device_exit' (function is undefined)
Removed calls to 'flexcop_device_kfree' (function is undefined)
Defining function usb_register_driver as symbolic
Removed calls to 'usb_kill_urb' (function is undefined)
Removed calls to 'usb_free_urb' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Defining function printk as symbolic
Defining function dev_set_drvdata as symbolic
Defining function dev_get_drvdata as symbolic
Defining function flexcop_device_kmalloc as symbolic
Defining function flexcop_device_initialize as symbolic
Defining function usb_alloc_urb as symbolic
Removed calls to 'flexcop_pass_dmx_packets' (function is undefined)
Defining function usb_submit_urb as symbolic
Defining function flexcop_sram_set_dest as symbolic
Defining function usb_set_interface as symbolic
Defining function usb_control_msg as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.163405895233
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 85 62 243 1174
INFO: Starting verification
KLEE: WARNING ONCE: function "flexcop_usb_transfer_exit" has inline asm
KLEE: ERROR: /tmp/symbiotic-rLvryF/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--b2c2--b2c2-flexcop-usb.ko-main.cil.out.c:6619: 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 18029 states (over memory cap)
KLEE: WARNING: killing 18589 states (over memory cap)
KLEE: WARNING: killing 18432 states (over memory cap)
KLEE: WARNING: killing 18572 states (over memory cap)
KLEE: WARNING: killing 18851 states (over memory cap)
KLEE: WARNING: killing 19146 states (over memory cap)
KLEE: WARNING: killing 19290 states (over memory cap)
KLEE: WARNING: killing 19303 states (over memory cap)
KLEE: WARNING: killing 13733 states (over memory cap)
KLEE: WARNING: killing 18696 states (over memory cap)
KLEE: WARNING: killing 18854 states (over memory cap)
KLEE: WARNING: killing 19010 states (over memory cap)
KLEE: WARNING: killing 13431 states (over memory cap)
KLEE: WARNING: killing 17881 states (over memory cap)
KLEE: WARNING: killing 13295 states (over memory cap)
KLEE: WARNING: killing 18238 states (over memory cap)
KLEE: WARNING: killing 18525 states (over memory cap)
KLEE: WARNING: killing 13224 states (over memory cap)
KLEE: WARNING: killing 17972 states (over memory cap)
KLEE: WARNING: killing 13230 states (over memory cap)
KLEE: WARNING: killing 17800 states (over memory cap)
KLEE: WARNING: killing 12984 states (over memory cap)
KLEE: WARNING: killing 17652 states (over memory cap)
KLEE: WARNING: killing 13122 states (over memory cap)
KLEE: WARNING: killing 17623 states (over memory cap)
KLEE: WARNING: killing 13010 states (over memory cap)
KLEE: WARNING: killing 17722 states (over memory cap)
KLEE: WARNING: killing 13026 states (over memory cap)
KLEE: WARNING: killing 17708 states (over memory cap)
KLEE: WARNING: killing 13044 states (over memory cap)
KLEE: WARNING: killing 12382 states (over memory cap)
KLEE: WARNING: killing 12463 states (over memory cap)
KLEE: WARNING: killing 17204 states (over memory cap)
KLEE: WARNING: killing 12851 states (over memory cap)
KLEE: WARNING: killing 12319 states (over memory cap)
KLEE: WARNING: killing 12284 states (over memory cap)
KLEE: WARNING: killing 12248 states (over memory cap)
KLEE: WARNING: killing 12330 states (over memory cap)
KLEE: WARNING: killing 12168 states (over memory cap)
KLEE: WARNING: killing 17055 states (over memory cap)
KLEE: WARNING: killing 12804 states (over memory cap)
KLEE: WARNING: killing 12287 states (over memory cap)
KLEE: WARNING: killing 12248 states (over memory cap)
KLEE: WARNING: killing 12212 states (over memory cap)
KLEE: WARNING: killing 12288 states (over memory cap)
KLEE: WARNING: killing 12256 states (over memory cap)
KLEE: WARNING: killing 12102 states (over memory cap)
KLEE: WARNING: killing 11945 states (over memory cap)
KLEE: WARNING: killing 12144 states (over memory cap)
KLEE: WARNING: killing 11991 states (over memory cap)
KLEE: WARNING: killing 12077 states (over memory cap)
KLEE: WARNING: killing 12275 states (over memory cap)
KLEE: WARNING: killing 12240 states (over memory cap)
KLEE: WARNING: killing 12093 states (over memory cap)
KLEE: WARNING: killing 12175 states (over memory cap)
KLEE: WARNING: killing 12137 states (over memory cap)
KLEE: WARNING: killing 11990 states (over memory cap)
KLEE: WARNING: killing 12183 states (over memory cap)
KLEE: WARNING: killing 12036 states (over memory cap)
KLEE: WARNING: killing 12113 states (over memory cap)
KLEE: WARNING: killing 11860 states (over memory cap)
KLEE: WARNING: killing 12050 states (over memory cap)
KLEE: WARNING: killing 12127 states (over memory cap)
KLEE: WARNING: killing 11988 states (over memory cap)
KLEE: WARNING: killing 11952 states (over memory cap)
KLEE: WARNING: killing 12033 states (over memory cap)
KLEE: WARNING: killing 12000 states (over memory cap)
KLEE: WARNING: killing 11742 states (over memory cap)
KLEE: WARNING: killing 12157 states (over memory cap)
KLEE: WARNING: killing 12016 states (over memory cap)
KLEE: WARNING: killing 11984 states (over memory cap)
KLEE: WARNING: killing 12176 states (over memory cap)
KLEE: WARNING: killing 12144 states (over memory cap)
KLEE: WARNING: killing 12003 states (over memory cap)
KLEE: WARNING: killing 11973 states (over memory cap)
KLEE: WARNING: killing 11936 states (over memory cap)
KLEE: WARNING: killing 11904 states (over memory cap)
KLEE: WARNING: killing 11873 states (over memory cap)
KLEE: WARNING: killing 11954 states (over memory cap)
KLEE: WARNING: killing 12134 states (over memory cap)
KLEE: WARNING: killing 11894 states (over memory cap)
KLEE: WARNING: killing 11970 states (over memory cap)
KLEE: WARNING: killing 11940 states (over memory cap)
KLEE: WARNING: killing 12012 states (over memory cap)
KLEE: WARNING: killing 11769 states (over memory cap)
KLEE: WARNING: killing 11847 states (over memory cap)
KLEE: WARNING: killing 11924 states (over memory cap)
KLEE: WARNING: killing 11999 states (over memory cap)
KLEE: WARNING: killing 12079 states (over memory cap)
