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--dvb-usb-v2--dvb-usb-mxl111sf.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.: 287 153 2800 14523
INFO: Compilation, preparation and instrumentation time: 0.501570940018
Removed calls to 'msleep' (function is undefined)
Defining function printk as symbolic
Defining function dvb_usbv2_generic_write as symbolic
Defining function dvb_usbv2_generic_rw as symbolic
Defining function dvb_usbv2_probe as symbolic
Defining function dvb_usbv2_suspend as symbolic
Defining function dvb_usbv2_resume as symbolic
Removed calls to '__symbol_put' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'tveeprom_hauppauge_analog' (function is undefined)
Defining function tveeprom_read as symbolic
Defining function __symbol_get as symbolic
Defining function __request_module as symbolic
Defining function usb_set_interface as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Defining function i2c_transfer as symbolic
Defining function mutex_lock_interruptible as symbolic
Defining function dev_get_drvdata as symbolic
Removed calls to 'usb_deregister' (function is undefined)
Defining function ldv_mxl111sf_props_mh_setup as symbolic
Defining function ldv_mxl111sf_props_mh_release as symbolic
Defining function ldv_mxl111sf_props_atsc_mh_setup as symbolic
Defining function ldv_mxl111sf_props_atsc_mh_release as symbolic
Defining function ldv_mxl111sf_props_mercury_mh_setup as symbolic
Defining function ldv_mxl111sf_props_mercury_mh_release as symbolic
Defining function ldv_mxl_tuner_config_release as symbolic
Defining function ldv_mxl_tuner_config_probe as symbolic
Defining function ldv_mxl111sf_props_mercury_setup as symbolic
Defining function ldv_mxl111sf_props_mercury_release as symbolic
Defining function ldv_mxl_demod_config_release as symbolic
Defining function ldv_mxl_demod_config_probe as symbolic
Defining function ldv_mxl111sf_props_dvbt_setup as symbolic
Defining function ldv_mxl111sf_props_dvbt_release as symbolic
Defining function ldv_mxl111sf_props_atsc_setup as symbolic
Defining function ldv_mxl111sf_props_atsc_release as symbolic
Defining function usb_register_driver as symbolic
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.502561807632
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 371 164 1446 8682
INFO: Starting verification
KLEE: WARNING: undefined reference to function: dvb_usbv2_disconnect
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:6567: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:7023: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:6845: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:8109: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:7219: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:7951: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:8162: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:6896: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:6965: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:8759: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:8570: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:8526: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:8707: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:8924: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:8874: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:8818: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:8657: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:8613: 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-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:6414: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22182 states (over memory cap)
KLEE: WARNING: killing 16230 states (over memory cap)
KLEE: WARNING: killing 15318 states (over memory cap)
KLEE: WARNING: killing 15466 states (over memory cap)
KLEE: WARNING: killing 15325 states (over memory cap)
KLEE: WARNING: killing 15095 states (over memory cap)
KLEE: WARNING: killing 15435 states (over memory cap)
KLEE: WARNING: killing 14821 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-vVtXgL/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--usb--dvb-usb-v2--dvb-usb-mxl111sf.ko-main.cil.out.c:6476: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15446 states (over memory cap)
KLEE: WARNING: killing 16258 states (over memory cap)
KLEE: WARNING: killing 16036 states (over memory cap)
KLEE: WARNING: killing 15624 states (over memory cap)
KLEE: WARNING: killing 16059 states (over memory cap)
KLEE: WARNING: killing 16308 states (over memory cap)
KLEE: WARNING: killing 16469 states (over memory cap)
KLEE: WARNING: killing 17005 states (over memory cap)
KLEE: WARNING: killing 16513 states (over memory cap)
KLEE: WARNING: killing 17517 states (over memory cap)
KLEE: WARNING: killing 17024 states (over memory cap)
KLEE: WARNING: killing 17183 states (over memory cap)
KLEE: WARNING: killing 17068 states (over memory cap)
KLEE: WARNING: killing 17883 states (over memory cap)
KLEE: WARNING: killing 17668 states (over memory cap)
KLEE: WARNING: killing 17187 states (over memory cap)
KLEE: WARNING: killing 17443 states (over memory cap)
KLEE: WARNING: killing 16305 states (over memory cap)
KLEE: WARNING: killing 16557 states (over memory cap)
KLEE: WARNING: killing 16069 states (over memory cap)
KLEE: WARNING: killing 16045 states (over memory cap)
KLEE: WARNING: killing 15744 states (over memory cap)
KLEE: WARNING: killing 16447 states (over memory cap)
KLEE: WARNING: killing 16057 states (over memory cap)
KLEE: WARNING: killing 15935 states (over memory cap)
KLEE: WARNING: killing 16184 states (over memory cap)
KLEE: WARNING: killing 15974 states (over memory cap)
KLEE: WARNING: killing 15951 states (over memory cap)
KLEE: WARNING: killing 15833 states (over memory cap)
KLEE: WARNING: killing 15903 states (over memory cap)
KLEE: WARNING: killing 15968 states (over memory cap)
KLEE: WARNING: killing 16302 states (over memory cap)
KLEE: WARNING: killing 16191 states (over memory cap)
KLEE: WARNING: killing 16252 states (over memory cap)
KLEE: WARNING: killing 16239 states (over memory cap)
KLEE: WARNING: killing 15940 states (over memory cap)
KLEE: WARNING: killing 16550 states (over memory cap)
KLEE: WARNING: killing 16167 states (over memory cap)
KLEE: WARNING: killing 16955 states (over memory cap)
KLEE: WARNING: killing 16131 states (over memory cap)
KLEE: WARNING: killing 16648 states (over memory cap)
KLEE: WARNING: killing 16537 states (over memory cap)
KLEE: WARNING: killing 16781 states (over memory cap)
KLEE: WARNING: killing 16494 states (over memory cap)
KLEE: WARNING: killing 16211 states (over memory cap)
KLEE: WARNING: killing 16097 states (over memory cap)
KLEE: WARNING: killing 16349 states (over memory cap)
KLEE: WARNING: killing 17034 states (over memory cap)
KLEE: WARNING: killing 16575 states (over memory cap)
KLEE: WARNING: killing 16556 states (over memory cap)
KLEE: WARNING: killing 15821 states (over memory cap)
KLEE: WARNING: killing 16240 states (over memory cap)
KLEE: WARNING: killing 15870 states (over memory cap)
KLEE: WARNING: killing 15317 states (over memory cap)
KLEE: WARNING: killing 16265 states (over memory cap)
KLEE: WARNING: killing 16065 states (over memory cap)
KLEE: WARNING: killing 15873 states (over memory cap)
KLEE: WARNING: killing 16107 states (over memory cap)
KLEE: WARNING: killing 16093 states (over memory cap)
KLEE: WARNING: killing 16858 states (over memory cap)
KLEE: WARNING: killing 15969 states (over memory cap)
KLEE: WARNING: killing 17088 states (over memory cap)
KLEE: WARNING: killing 16896 states (over memory cap)
KLEE: WARNING: killing 16789 states (over memory cap)
KLEE: WARNING: killing 16425 states (over memory cap)
KLEE: WARNING: killing 15629 states (over memory cap)
KLEE: WARNING: killing 16217 states (over memory cap)
KLEE: WARNING: killing 16460 states (over memory cap)
KLEE: WARNING: killing 16527 states (over memory cap)
KLEE: WARNING: killing 16768 states (over memory cap)
KLEE: WARNING: killing 16228 states (over memory cap)
KLEE: WARNING: killing 16205 states (over memory cap)
KLEE: WARNING: killing 15589 states (over memory cap)
KLEE: WARNING: killing 16516 states (over memory cap)
KLEE: WARNING: killing 16325 states (over memory cap)
KLEE: WARNING: killing 15957 states (over memory cap)
KLEE: WARNING: killing 15680 states (over memory cap)
KLEE: WARNING: killing 16267 states (over memory cap)
KLEE: WARNING: killing 16159 states (over memory cap)
KLEE: WARNING: killing 16735 states (over memory cap)
KLEE: WARNING: killing 15952 states (over memory cap)
KLEE: WARNING: killing 16194 states (over memory cap)
KLEE: WARNING: killing 16687 states (over memory cap)
KLEE: WARNING: killing 15819 states (over memory cap)
KLEE: WARNING: killing 16145 states (over memory cap)
KLEE: WARNING: killing 15869 states (over memory cap)
KLEE: WARNING: killing 16448 states (over memory cap)
KLEE: WARNING: killing 16686 states (over memory cap)
KLEE: WARNING: killing 16412 states (over memory cap)
KLEE: WARNING: killing 16395 states (over memory cap)
KLEE: WARNING: killing 16289 states (over memory cap)
KLEE: WARNING: killing 15599 states (over memory cap)
KLEE: WARNING: killing 16256 states (over memory cap)
KLEE: WARNING: killing 15904 states (over memory cap)
KLEE: WARNING: killing 15803 states (over memory cap)
KLEE: WARNING: killing 16455 states (over memory cap)
KLEE: WARNING: killing 16434 states (over memory cap)
KLEE: WARNING: killing 16170 states (over memory cap)
KLEE: WARNING: killing 15646 states (over memory cap)
KLEE: WARNING: killing 16472 states (over memory cap)
KLEE: WARNING: killing 16454 states (over memory cap)
KLEE: WARNING: killing 16433 states (over memory cap)
KLEE: WARNING: killing 15334 states (over memory cap)
KLEE: WARNING: killing 16483 states (over memory cap)
KLEE: WARNING: killing 16131 states (over memory cap)
KLEE: WARNING: killing 16119 states (over memory cap)
KLEE: WARNING: killing 16018 states (over memory cap)
KLEE: WARNING: killing 15749 states (over memory cap)
KLEE: WARNING: killing 16394 states (over memory cap)
KLEE: WARNING: killing 16460 states (over memory cap)
KLEE: WARNING: killing 16275 states (over memory cap)
KLEE: WARNING: killing 16095 states (over memory cap)
KLEE: WARNING: killing 16411 states (over memory cap)
KLEE: WARNING: killing 16385 states (over memory cap)
KLEE: WARNING: killing 16370 states (over memory cap)
KLEE: WARNING: killing 16769 states (over memory cap)
KLEE: WARNING: killing 16505 states (over memory cap)
KLEE: WARNING: killing 16239 states (over memory cap)
KLEE: WARNING: killing 15569 states (over memory cap)
KLEE: WARNING: killing 15961 states (over memory cap)
KLEE: WARNING: killing 16516 states (over memory cap)
KLEE: WARNING: killing 16332 states (over memory cap)
KLEE: WARNING: killing 16562 states (over memory cap)
KLEE: WARNING: killing 16461 states (over memory cap)
KLEE: WARNING: killing 15784 states (over memory cap)
KLEE: WARNING: killing 16179 states (over memory cap)
KLEE: WARNING: killing 16572 states (over memory cap)
KLEE: WARNING: killing 16471 states (over memory cap)
KLEE: WARNING: killing 15890 states (over memory cap)
KLEE: WARNING: killing 16927 states (over memory cap)
KLEE: WARNING: killing 16185 states (over memory cap)
KLEE: WARNING: killing 15843 states (over memory cap)
KLEE: WARNING: killing 16637 states (over memory cap)
KLEE: WARNING: killing 16288 states (over memory cap)
KLEE: WARNING: killing 15948 states (over memory cap)
KLEE: WARNING: killing 15931 states (over memory cap)
KLEE: WARNING: killing 16324 states (over memory cap)
KLEE: WARNING: killing 16229 states (over memory cap)
KLEE: WARNING: killing 16367 states (over memory cap)
KLEE: WARNING: killing 16271 states (over memory cap)
KLEE: WARNING: killing 16099 states (over memory cap)
KLEE: WARNING: killing 16318 states (over memory cap)
KLEE: WARNING: killing 15982 states (over memory cap)
KLEE: WARNING: killing 16127 states (over memory cap)
KLEE: WARNING: killing 16191 states (over memory cap)
KLEE: WARNING: killing 15929 states (over memory cap)
KLEE: WARNING: killing 15832 states (over memory cap)
KLEE: WARNING: killing 16127 states (over memory cap)
KLEE: WARNING: killing 16271 states (over memory cap)
KLEE: WARNING: killing 16088 states (over memory cap)
KLEE: WARNING: killing 16233 states (over memory cap)
KLEE: WARNING: killing 16537 states (over memory cap)
KLEE: WARNING: killing 16125 states (over memory cap)
KLEE: WARNING: killing 16105 states (over memory cap)
