bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.14/linux-3.14__complex_emg__linux-usb-dev__drivers-media-usb-dvb-usb-dvb-usb-dib0700_true-unreach-call.cil.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.: 1043 576 4538 26671
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.15884113312
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Defining function usb_register_driver as symbolic
Defining function ldv_pre_usb_register_driver as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to '__symbol_put' (function is undefined)
Removed calls to 'rc_keydown' (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 mutex_lock_interruptible_nested as symbolic
Defining function usb_control_msg as symbolic
Defining function dib8000_i2c_enumeration 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 dibx000_i2c_set_speed as symbolic
Defining function i2c_transfer as symbolic
Defining function request_firmware 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 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 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
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 usb_bulk_msg as symbolic
Defining function dvb_usb_get_hexline as symbolic
Defining function dib7090_get_adc_power as symbolic
Defining function dib7090_tuner_sleep as symbolic
Defining function dib8000_get_adc_power as symbolic
Defining function dib8096p_tuner_sleep as symbolic
Removed calls to 'dib0090_set_dc_servo' (function is undefined)
Defining function dib7000p_set_agc1_min as symbolic
Defining function dvb_usb_device_init as symbolic
Removed calls to 'dib0090_dcc_freq' (function is undefined)
Defining function external_allocated_data as symbolic
Removed calls to 'dvb_usb_device_exit' (function is undefined)
Removed calls to 'ldv_pre_probe' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
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.964807033539
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1127 610 2056 14830
INFO: Starting verification
KLEE: WARNING: undefined reference to function: dib0070_ctrl_agc_filter
KLEE: WARNING: undefined reference to function: dvb_usb_device_exit
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_9ffb03e3-0d41-4f52-80cd-d5bfcefd06cc/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16268 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 29641 states (over memory cap)
KLEE: WARNING: killing 28262 states (over memory cap)
KLEE: WARNING: killing 27037 states (over memory cap)
KLEE: WARNING: killing 26262 states (over memory cap)
KLEE: WARNING: killing 25903 states (over memory cap)
KLEE: WARNING: killing 26117 states (over memory cap)
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING: killing 26334 states (over memory cap)
KLEE: WARNING: killing 25595 states (over memory cap)
KLEE: WARNING: killing 25407 states (over memory cap)
KLEE: WARNING: killing 25079 states (over memory cap)
KLEE: WARNING: killing 25030 states (over memory cap)
KLEE: WARNING: killing 25556 states (over memory cap)
KLEE: WARNING: killing 24689 states (over memory cap)
KLEE: WARNING: killing 27541 states (over memory cap)
KLEE: WARNING: killing 25295 states (over memory cap)
KLEE: WARNING: killing 25802 states (over memory cap)
KLEE: WARNING: killing 25622 states (over memory cap)
KLEE: WARNING: killing 26263 states (over memory cap)
KLEE: WARNING: killing 28272 states (over memory cap)
KLEE: WARNING: killing 27690 states (over memory cap)
KLEE: WARNING: killing 28594 states (over memory cap)
KLEE: WARNING: killing 28699 states (over memory cap)
KLEE: WARNING: killing 30283 states (over memory cap)
KLEE: WARNING: killing 30388 states (over memory cap)
KLEE: WARNING: killing 31973 states (over memory cap)
KLEE: WARNING: killing 30446 states (over memory cap)
KLEE: WARNING: killing 30945 states (over memory cap)
KLEE: WARNING: killing 31840 states (over memory cap)
KLEE: WARNING: killing 32483 states (over memory cap)
KLEE: WARNING: killing 32185 states (over memory cap)
KLEE: WARNING: killing 29293 states (over memory cap)
KLEE: WARNING: killing 30602 states (over memory cap)
KLEE: WARNING: killing 30014 states (over memory cap)
KLEE: WARNING: killing 31194 states (over memory cap)
KLEE: WARNING: killing 29132 states (over memory cap)
KLEE: WARNING: killing 29372 states (over memory cap)
KLEE: WARNING: killing 29339 states (over memory cap)
KLEE: WARNING: killing 26891 states (over memory cap)
KLEE: WARNING: killing 28982 states (over memory cap)
KLEE: WARNING: killing 27622 states (over memory cap)
KLEE: WARNING: killing 27057 states (over memory cap)
KLEE: WARNING: killing 27282 states (over memory cap)
KLEE: WARNING: killing 28841 states (over memory cap)
KLEE: WARNING: killing 28936 states (over memory cap)
KLEE: WARNING: killing 27575 states (over memory cap)
KLEE: WARNING: killing 29260 states (over memory cap)
KLEE: WARNING: killing 29355 states (over memory cap)
KLEE: WARNING: killing 29601 states (over memory cap)
KLEE: WARNING: killing 27575 states (over memory cap)
KLEE: WARNING: killing 28466 states (over memory cap)
KLEE: WARNING: killing 27499 states (over memory cap)
KLEE: WARNING: killing 28660 states (over memory cap)
KLEE: WARNING: killing 30066 states (over memory cap)
KLEE: WARNING: killing 28594 states (over memory cap)
KLEE: WARNING: killing 29087 states (over memory cap)
KLEE: WARNING: killing 28674 states (over memory cap)
KLEE: WARNING: killing 30075 states (over memory cap)
KLEE: WARNING: killing 29397 states (over memory cap)
KLEE: WARNING: killing 28717 states (over memory cap)
KLEE: WARNING: killing 28416 states (over memory cap)
KLEE: WARNING: killing 28913 states (over memory cap)
KLEE: WARNING: killing 29396 states (over memory cap)
KLEE: WARNING: killing 29378 states (over memory cap)
KLEE: WARNING: killing 29736 states (over memory cap)
KLEE: WARNING: killing 28790 states (over memory cap)
KLEE: WARNING: killing 28487 states (over memory cap)
KLEE: WARNING: killing 29358 states (over memory cap)
KLEE: WARNING: killing 28693 states (over memory cap)
KLEE: WARNING: killing 26980 states (over memory cap)
KLEE: WARNING: killing 28100 states (over memory cap)
KLEE: WARNING: killing 28981 states (over memory cap)
KLEE: WARNING: killing 28439 states (over memory cap)
KLEE: WARNING: killing 28798 states (over memory cap)
KLEE: WARNING: killing 27731 states (over memory cap)
KLEE: WARNING: killing 29643 states (over memory cap)
KLEE: WARNING: killing 30642 states (over memory cap)
KLEE: WARNING: killing 29058 states (over memory cap)
KLEE: WARNING: killing 28524 states (over memory cap)
KLEE: WARNING: killing 26957 states (over memory cap)
KLEE: WARNING: killing 28838 states (over memory cap)
KLEE: WARNING: killing 28552 states (over memory cap)
KLEE: WARNING: killing 29036 states (over memory cap)
KLEE: WARNING: killing 30165 states (over memory cap)
KLEE: WARNING: killing 29497 states (over memory cap)
KLEE: WARNING: killing 29726 states (over memory cap)
KLEE: WARNING: killing 29563 states (over memory cap)
KLEE: WARNING: killing 29670 states (over memory cap)
KLEE: WARNING: killing 28101 states (over memory cap)
KLEE: WARNING: killing 27809 states (over memory cap)
KLEE: WARNING: killing 29050 states (over memory cap)
KLEE: WARNING: killing 30152 states (over memory cap)
KLEE: WARNING: killing 28742 states (over memory cap)
KLEE: WARNING: killing 28440 states (over memory cap)
KLEE: WARNING: killing 29294 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-wg4iSF/linux-3.14__complex_emg__linux-usb-dev__drivers-media-usb-dvb-usb-dvb-usb-dib0700_true-unreach-call.cil.c:7224: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 28253 states (over memory cap)
KLEE: WARNING: killing 28854 states (over memory cap)
KLEE: WARNING: killing 29459 states (over memory cap)
KLEE: WARNING: killing 29041 states (over memory cap)
KLEE: WARNING: killing 28502 states (over memory cap)
KLEE: WARNING: killing 29740 states (over memory cap)
KLEE: WARNING: killing 28454 states (over memory cap)
KLEE: WARNING: killing 29163 states (over memory cap)
KLEE: WARNING: killing 29385 states (over memory cap)
KLEE: WARNING: killing 27724 states (over memory cap)
KLEE: WARNING: killing 27824 states (over memory cap)
KLEE: WARNING: killing 30524 states (over memory cap)
KLEE: WARNING: killing 30132 states (over memory cap)
KLEE: WARNING: killing 29224 states (over memory cap)
KLEE: WARNING: killing 27829 states (over memory cap)
KLEE: WARNING: killing 27555 states (over memory cap)
KLEE: WARNING: killing 29248 states (over memory cap)
KLEE: WARNING: killing 28114 states (over memory cap)
KLEE: WARNING: killing 29570 states (over memory cap)
KLEE: WARNING: killing 28684 states (over memory cap)
KLEE: WARNING: killing 28643 states (over memory cap)
KLEE: WARNING: killing 29105 states (over memory cap)
KLEE: WARNING: killing 30068 states (over memory cap)
KLEE: WARNING: killing 28804 states (over memory cap)
KLEE: WARNING: killing 29877 states (over memory cap)
KLEE: WARNING: killing 29346 states (over memory cap)
KLEE: WARNING: killing 28708 states (over memory cap)
KLEE: WARNING: killing 28177 states (over memory cap)
KLEE: WARNING: killing 28148 states (over memory cap)
KLEE: WARNING: killing 27982 states (over memory cap)
KLEE: WARNING: killing 28690 states (over memory cap)
KLEE: WARNING: killing 29269 states (over memory cap)
KLEE: WARNING: killing 29478 states (over memory cap)
KLEE: WARNING: killing 28853 states (over memory cap)
KLEE: WARNING: killing 27716 states (over memory cap)
