bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-challenges/linux-3.14__complex_emg__linux-alloc-spinlock__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.: 1057 654 4775 27865
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.99106502533
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 'ldv_after_alloc' (function is undefined)
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 'usb_free_urb' (function is undefined)
Defining function external_allocated_data 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)
Removed calls to 'ldv_assert' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'dvb_usb_device_exit' (function is undefined)
Removed calls to 'ldv_pre_probe' (function is undefined)
Linked our definitions to these undefined functions:
  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.831210136414
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1135 683 2173 15688
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_0b48f2f9-6b82-4ab9-aaa6-68da2dec0742/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 41358 states (over memory cap)
KLEE: WARNING: killing 29724 states (over memory cap)
KLEE: WARNING: killing 29062 states (over memory cap)
KLEE: WARNING: killing 29105 states (over memory cap)
KLEE: WARNING: killing 27167 states (over memory cap)
KLEE: WARNING: killing 25953 states (over memory cap)
KLEE: WARNING: killing 26588 states (over memory cap)
KLEE: WARNING: killing 25966 states (over memory cap)
KLEE: WARNING: killing 23510 states (over memory cap)
KLEE: WARNING: killing 26412 states (over memory cap)
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING: killing 25112 states (over memory cap)
KLEE: WARNING: killing 26192 states (over memory cap)
KLEE: WARNING: killing 26847 states (over memory cap)
KLEE: WARNING: killing 26674 states (over memory cap)
KLEE: WARNING: killing 25372 states (over memory cap)
KLEE: WARNING: killing 25607 states (over memory cap)
KLEE: WARNING: killing 25843 states (over memory cap)
KLEE: WARNING: killing 27059 states (over memory cap)
KLEE: WARNING: killing 27006 states (over memory cap)
KLEE: WARNING: killing 28356 states (over memory cap)
KLEE: WARNING: killing 29285 states (over memory cap)
KLEE: WARNING: killing 29519 states (over memory cap)
KLEE: WARNING: killing 30304 states (over memory cap)
KLEE: WARNING: killing 30961 states (over memory cap)
KLEE: WARNING: killing 30917 states (over memory cap)
KLEE: WARNING: killing 31000 states (over memory cap)
KLEE: WARNING: killing 30128 states (over memory cap)
KLEE: WARNING: killing 31737 states (over memory cap)
KLEE: WARNING: killing 30595 states (over memory cap)
KLEE: WARNING: killing 29996 states (over memory cap)
KLEE: WARNING: killing 32152 states (over memory cap)
KLEE: WARNING: killing 29245 states (over memory cap)
KLEE: WARNING: killing 30697 states (over memory cap)
KLEE: WARNING: killing 31069 states (over memory cap)
KLEE: WARNING: killing 30078 states (over memory cap)
KLEE: WARNING: killing 28813 states (over memory cap)
KLEE: WARNING: killing 29046 states (over memory cap)
KLEE: WARNING: killing 29697 states (over memory cap)
KLEE: WARNING: killing 28705 states (over memory cap)
KLEE: WARNING: killing 28526 states (over memory cap)
KLEE: WARNING: killing 27548 states (over memory cap)
KLEE: WARNING: killing 28980 states (over memory cap)
KLEE: WARNING: killing 27741 states (over memory cap)
KLEE: WARNING: killing 27033 states (over memory cap)
KLEE: WARNING: killing 28615 states (over memory cap)
KLEE: WARNING: killing 27910 states (over memory cap)
KLEE: WARNING: killing 28551 states (over memory cap)
KLEE: WARNING: killing 27850 states (over memory cap)
KLEE: WARNING: killing 28219 states (over memory cap)
KLEE: WARNING: killing 28857 states (over memory cap)
KLEE: WARNING: killing 29219 states (over memory cap)
KLEE: WARNING: killing 29058 states (over memory cap)
KLEE: WARNING: killing 29566 states (over memory cap)
KLEE: WARNING: killing 30058 states (over memory cap)
KLEE: WARNING: killing 28305 states (over memory cap)
KLEE: WARNING: killing 28406 states (over memory cap)
KLEE: WARNING: killing 28903 states (over memory cap)
KLEE: WARNING: killing 29525 states (over memory cap)
KLEE: WARNING: killing 28968 states (over memory cap)
KLEE: WARNING: killing 28007 states (over memory cap)
KLEE: WARNING: killing 28634 states (over memory cap)
KLEE: WARNING: killing 30331 states (over memory cap)
KLEE: WARNING: killing 28713 states (over memory cap)
KLEE: WARNING: killing 27886 states (over memory cap)
KLEE: WARNING: killing 28376 states (over memory cap)
KLEE: WARNING: killing 28740 states (over memory cap)
KLEE: WARNING: killing 28964 states (over memory cap)
KLEE: WARNING: killing 29337 states (over memory cap)
KLEE: WARNING: killing 28514 states (over memory cap)
KLEE: WARNING: killing 29146 states (over memory cap)
KLEE: WARNING: killing 29510 states (over memory cap)
KLEE: WARNING: killing 28179 states (over memory cap)
KLEE: WARNING: killing 27615 states (over memory cap)
KLEE: WARNING: killing 29424 states (over memory cap)
KLEE: WARNING: killing 27834 states (over memory cap)
KLEE: WARNING: killing 30012 states (over memory cap)
KLEE: WARNING: killing 29597 states (over memory cap)
KLEE: WARNING: killing 28257 states (over memory cap)
KLEE: WARNING: killing 27065 states (over memory cap)
KLEE: WARNING: killing 29877 states (over memory cap)
KLEE: WARNING: killing 29463 states (over memory cap)
KLEE: WARNING: killing 29177 states (over memory cap)
KLEE: WARNING: killing 28378 states (over memory cap)
KLEE: WARNING: killing 29252 states (over memory cap)
KLEE: WARNING: killing 27805 states (over memory cap)
KLEE: WARNING: killing 28015 states (over memory cap)
KLEE: WARNING: killing 29149 states (over memory cap)
KLEE: WARNING: killing 29249 states (over memory cap)
KLEE: WARNING: killing 29872 states (over memory cap)
KLEE: WARNING: killing 30474 states (over memory cap)
KLEE: WARNING: killing 28909 states (over memory cap)
KLEE: WARNING: killing 29258 states (over memory cap)
KLEE: WARNING: killing 26782 states (over memory cap)
KLEE: WARNING: killing 29056 states (over memory cap)
KLEE: WARNING: killing 28901 states (over memory cap)
KLEE: WARNING: killing 29001 states (over memory cap)
KLEE: WARNING: killing 28198 states (over memory cap)
KLEE: WARNING: killing 28926 states (over memory cap)
KLEE: WARNING: killing 28139 states (over memory cap)
KLEE: WARNING: killing 27719 states (over memory cap)
KLEE: WARNING: killing 27687 states (over memory cap)
KLEE: WARNING: killing 29184 states (over memory cap)
KLEE: WARNING: killing 29158 states (over memory cap)
KLEE: WARNING: killing 28752 states (over memory cap)
KLEE: WARNING: killing 29747 states (over memory cap)
KLEE: WARNING: killing 28963 states (over memory cap)
KLEE: WARNING: killing 29180 states (over memory cap)
KLEE: WARNING: killing 28395 states (over memory cap)
KLEE: WARNING: killing 28614 states (over memory cap)
KLEE: WARNING: killing 29955 states (over memory cap)
KLEE: WARNING: killing 29807 states (over memory cap)
KLEE: WARNING: killing 29654 states (over memory cap)
KLEE: WARNING: killing 27603 states (over memory cap)
KLEE: WARNING: killing 28821 states (over memory cap)
KLEE: WARNING: killing 27796 states (over memory cap)
KLEE: WARNING: killing 30507 states (over memory cap)
KLEE: WARNING: killing 28229 states (over memory cap)
KLEE: WARNING: killing 28697 states (over memory cap)
KLEE: WARNING: killing 29160 states (over memory cap)
KLEE: WARNING: killing 30011 states (over memory cap)
KLEE: WARNING: killing 28481 states (over memory cap)
KLEE: WARNING: killing 27694 states (over memory cap)
KLEE: WARNING: killing 27421 states (over memory cap)
KLEE: WARNING: killing 27893 states (over memory cap)
KLEE: WARNING: killing 30705 states (over memory cap)
KLEE: WARNING: killing 28947 states (over memory cap)
KLEE: WARNING: killing 29044 states (over memory cap)
KLEE: WARNING: killing 29252 states (over memory cap)
KLEE: WARNING: killing 27749 states (over memory cap)
KLEE: WARNING: killing 30185 states (over memory cap)
KLEE: WARNING: killing 29774 states (over memory cap)
KLEE: WARNING: killing 28131 states (over memory cap)
KLEE: WARNING: killing 28465 states (over memory cap)
KLEE: WARNING: killing 28309 states (over memory cap)
KLEE: WARNING: killing 29006 states (over memory cap)
KLEE: WARNING: killing 27874 states (over memory cap)
KLEE: WARNING: killing 29429 states (over memory cap)
