bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.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.: 308 119 2253 35870
INFO: Compilation, preparation and instrumentation time: 1.23380899429
Removed calls to 'msleep' (function is undefined)
Removed calls to '__symbol_put' (function is undefined)
Removed calls to 'rc_keydown' (function is undefined)
Removed calls to 'release_firmware' (function is undefined)
Defining function dib8096p_get_i2c_tuner as symbolic
Defining function __symbol_get as symbolic
Defining function __request_module as symbolic
Defining function printk as symbolic
Defining function dib8000_set_gpio as symbolic
Removed calls to 'dib0090_pwm_gain_reset' (function is undefined)
Defining function dib0090_get_wbd_target as symbolic
Defining function dib8000_set_wbd_ref as symbolic
Defining function dib8000_update_pll as symbolic
Defining function dib8000_ctrl_timf as symbolic
Defining function dib8000_i2c_enumeration as symbolic
Defining function usb_control_msg as symbolic
Defining function dib7090_get_i2c_tuner as symbolic
Defining function dib7000p_set_gpio as symbolic
Defining function dib7000p_set_wbd_ref as symbolic
Defining function dib7000p_update_pll as symbolic
Defining function dib7000p_ctrl_timf as symbolic
Defining function dib7000p_i2c_enumeration as symbolic
Defining function dib7000p_get_i2c_master as symbolic
Defining function dib7000pc_detection as symbolic
Defining function dib7090_slave_reset as symbolic
Defining function dib9000_get_tuner_interface as symbolic
Defining function dib9000_get_i2c_master as symbolic
Defining function dib9000_firmware_post_pll_init as symbolic
Defining function dib9000_get_slave_frontend as symbolic
Defining function dib9000_get_component_bus_interface as symbolic
Defining function dib9000_set_i2c_adapter as symbolic
Defining function dib9000_fw_set_component_bus_speed as symbolic
Defining function dibx000_i2c_set_speed as symbolic
Defining function i2c_transfer as symbolic
Defining function request_firmware as symbolic
Defining function dib9000_i2c_enumeration as symbolic
Defining function dib9000_set_slave_frontend as symbolic
Defining function dib8000_get_slave_frontend as symbolic
Defining function dib8000_get_i2c_master as symbolic
Removed calls to 'dib0090_get_current_gain' (function is undefined)
Removed calls to 'dib8000_pwm_agc_reset' (function is undefined)
Defining function dib0090_set_tune_state as symbolic
Defining function dib0090_gain_control as symbolic
Defining function dib0090_get_tune_state as symbolic
Defining function dib8000_set_tune_state as symbolic
Defining function dib8000_set_slave_frontend as symbolic
Defining function dib9000_fw_pid_filter as symbolic
Defining function dib9000_fw_pid_filter_ctrl as symbolic
Defining function dib0070_wbd_offset as symbolic
Defining function dib8000_pid_filter as symbolic
Defining function dib8000_pid_filter_ctrl as symbolic
Defining function dib7000p_pid_filter as symbolic
Defining function dib7000p_pid_filter_ctrl as symbolic
Defining function dib3000mc_get_tuner_i2c_master as symbolic
Defining function dib3000mc_i2c_enumeration as symbolic
Removed calls to 'usb_free_urb' (function is undefined)
Defining function usb_alloc_urb as symbolic
Defining function usb_submit_urb as symbolic
Defining function dib7000m_get_i2c_master as symbolic
Defining function dib7000m_pid_filter as symbolic
Defining function dib7000m_pid_filter_ctrl as symbolic
Defining function dvb_usb_get_hexline as symbolic
Defining function usb_bulk_msg as symbolic
Defining function dvb_usb_device_init as symbolic
Defining function dib8000_get_adc_power as symbolic
Defining function dib9000_set_gpio as symbolic
Removed calls to 'dib0090_set_dc_servo' (function is undefined)
Defining function dib7090_tuner_sleep as symbolic
Defining function dib7090_get_adc_power as symbolic
Defining function dib0090_get_wbd_offset as symbolic
Defining function dib7000p_get_agc_values as symbolic
Defining function dib0090_set_switch as symbolic
Defining function dib0090_set_vga as symbolic
Defining function dib0090_update_rframp_7090 as symbolic
Defining function dib0090_update_tuning_table_7090 as symbolic
Defining function dib8096p_tuner_sleep as symbolic
Defining function dev_get_drvdata as symbolic
Defining function usb_register_driver as symbolic
Removed calls to 'usb_deregister' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Linked our definitions to these undefined functions:
  __kmalloc
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.667069911957
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 453 181 1095 12992
INFO: Starting verification
KLEE: WARNING: undefined reference to function: dib0070_ctrl_agc_filter
KLEE: WARNING: undefined reference to function: dib0090_dcc_freq
KLEE: WARNING: undefined reference to function: dvb_usb_device_exit
KLEE: WARNING ONCE: flushing 88800 bytes on read, may be slow and/or crash: MO90[88800] allocated at global:dib0700_devices
KLEE: ERROR: /tmp/symbiotic-Fsism2/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:8616: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Fsism2/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11252: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Fsism2/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:8622: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Fsism2/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6663: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Fsism2/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11288: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_5cbda21b-6a49-4242-93b3-6fed819766f3/symbiotic/lib/verifier/__VERIFIER_error.c:9: ASSERTION FAIL: verifier assertion failed
KLEE: NOTE: now ignoring this error at this location
Error found.
RESULT: false(unreach-call)

 --- Error trace ---

Error: ASSERTION FAIL: verifier assertion failed
File: /tmp/vcloud-vcloud-master/worker/working_dir_5cbda21b-6a49-4242-93b3-6fed819766f3/symbiotic/lib/verifier/__VERIFIER_error.c
Line: 9
assembly.ll line: 979
Stack: 
	#000000979 in __VERIFIER_error () at /tmp/vcloud-vcloud-master/worker/working_dir_5cbda21b-6a49-4242-93b3-6fed819766f3/symbiotic/lib/verifier/__VERIFIER_error.c:9
	#100007521 in ldv_blast_assert () at /tmp/symbiotic-Fsism2/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11547
	#200007378 in mutex_lock_interruptible (=0) at /tmp/symbiotic-Fsism2/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11560
	#300001490 in dib0700_i2c_xfer (, , ) at /tmp/symbiotic-Fsism2/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:8411
	#400010468 in main () at /tmp/symbiotic-Fsism2/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11502

 --- ----------- ---
Generating witness: /tmp/vcloud-vcloud-master/worker/working_dir_5cbda21b-6a49-4242-93b3-6fed819766f3/symbiotic/witness.graphml
 -- ---- --
Symbolic objects:
nondet := len 8 bytes, |8 times 0x0|
nondet:1 := len 8 bytes, |8 times 0x0|
nondet:2 := len 2 bytes, |2 times 0x0|
nondet:3 := len 4 bytes, |4 times 0x0|
nondet:4 := len 8 bytes, |0x50|0xa|0x24|0x4|4 times 0x0|
nondet:5 := len 8 bytes, |8 times 0x0|
nondet:6 := len 8 bytes, |8 times 0x0|
nondet:7 := len 8 bytes, |8 times 0x0|
nondet:8 := len 8 bytes, |8 times 0x0|
nondet:9 := len 8 bytes, |8 times 0x0|
nondet:10 := len 8 bytes, |8 times 0x0|
nondet:11 := len 8 bytes, |8 times 0x0|
nondet:12 := len 8 bytes, |8 times 0x0|
nondet:13 := len 8 bytes, |8 times 0x0|
nondet:14 := len 8 bytes, |8 times 0x0|
nondet:15 := len 8 bytes, |8 times 0x0|
nondet:16 := len 12 bytes, |12 times 0x0|
nondet:17 := len 32 bytes, |32 times 0x0|
nondet:18 := len 8 bytes, |8 times 0x0|
nondet:19 := len 8 bytes, |8 times 0x0|
nondet:20 := len 8 bytes, |8 times 0x0|
nondet:21 := len 8 bytes, |8 times 0x0|
nondet:22 := len 8 bytes, |8 times 0x0|
nondet:23 := len 8 bytes, |8 times 0x0|
nondet:24 := len 8 bytes, |8 times 0x0|
nondet:25 := len 8 bytes, |8 times 0x0|
nondet:26 := len 8 bytes, |8 times 0x0|
nondet:27 := len 8 bytes, |8 times 0x0|
nondet:28 := len 8 bytes, |8 times 0x0|
nondet:29 := len 8 bytes, |8 times 0x0|
nondet:30 := len 8 bytes, |8 times 0x0|
nondet:31 := len 8 bytes, |8 times 0x0|
nondet:32 := len 8 bytes, |8 times 0x0|
nondet:33 := len 8 bytes, |8 times 0x0|
nondet:34 := len 8 bytes, |8 times 0x0|
nondet:35 := len 8 bytes, |8 times 0x0|
nondet:36 := len 8 bytes, |8 times 0x0|
nondet:37 := len 8 bytes, |8 times 0x0|
nondet:38 := len 8 bytes, |8 times 0x0|
nondet:39 := len 8 bytes, |8 times 0x0|
nondet:40 := len 8 bytes, |8 times 0x0|
nondet:41 := len 8 bytes, |8 times 0x0|
nondet:42 := len 8 bytes, |8 times 0x0|
nondet:43 := len 8 bytes, |8 times 0x0|
nondet:44 := len 8 bytes, |8 times 0x0|
nondet:45 := len 8 bytes, |8 times 0x0|
nondet:46 := len 8 bytes, |8 times 0x0|
nondet:47 := len 8 bytes, |8 times 0x0|
nondet:48 := len 8 bytes, |8 times 0x0|
nondet:49 := len 8 bytes, |8 times 0x0|
nondet:50 := len 8 bytes, |8 times 0x0|
nondet:51 := len 8 bytes, |8 times 0x0|
nondet:52 := len 8 bytes, |8 times 0x0|
nondet:53 := len 8 bytes, |8 times 0x0|
nondet:54 := len 2 bytes, |2 times 0x0|
nondet:55 := len 1 bytes, |0x0|
nondet:56 := len 8 bytes, |8 times 0x0|
nondet:57 := len 8 bytes, |8 times 0x0|
nondet:58 := len 8 bytes, |8 times 0x0|
nondet:59 := len 8 bytes, |8 times 0x0|
nondet:60 := len 268 bytes, |268 times 0x0|
nondet:61 := len 4 bytes, |4 times 0x0|
extern-global:__this_module := len 600 bytes, |600 times 0x0|
extern-global:param_ops_short := len 24 bytes, |24 times 0x0|
extern-global:param_array_ops := len 24 bytes, |0x57|0x1d|0x24|0x4|4 times 0x0|16 times 0xff|
extern-global:param_ops_int := len 24 bytes, |24 times 0x0|
main:tmp___8:11471 := len 4 bytes, |4 times 0x1|
main:tmp___7:11486 := len 4 bytes, |4 times 0x0|
mutex_lock_interruptible:nondetermined:11564 := len 4 bytes, |4 times 0x1|
 -- ---- --
INFO: Total time elapsed: 427.742571115
