bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.12-rc1/linux-3.12-rc1.tar.xz-144_2a-drivers--media--usb--dvb-usb--dvb-usb-dib0700.ko-entry_point_false-unreach-call.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.: 334 175 1969 13903
Removed infinite loop in ldv_stop___1
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.711954832077
Removed calls to 'mutex_unlock' (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
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 dvb_usb_device_init as symbolic
Removed calls to 'dib0090_dcc_freq' (function is undefined)
Removed calls to 'dib0090_set_dc_servo' (function is undefined)
Defining function dib8000_get_adc_power as symbolic
Defining function dib7000p_set_agc1_min as symbolic
Defining function dib7090_tuner_sleep as symbolic
Defining function dib7090_get_adc_power as symbolic
Defining function dib8096p_tuner_sleep as symbolic
Defining function dev_get_drvdata as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'dvb_usb_device_exit' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Defining function usb_register_driver as symbolic
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.616600990295
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 441 208 1186 7627
INFO: Starting verification
KLEE: WARNING: undefined reference to function: __VERIFIER_nondet_u16_named
KLEE: WARNING: undefined reference to function: __VERIFIER_nondet_u8_named
KLEE: WARNING: undefined reference to function: dib0070_ctrl_agc_filter
KLEE: WARNING: undefined reference to function: dvb_usb_device_exit
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_7a5d59db-2c4f-4089-8e4f-909b9eda68af/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 24565 states (over memory cap)
KLEE: WARNING: killing 15159 states (over memory cap)
KLEE: WARNING: killing 14879 states (over memory cap)
KLEE: WARNING: killing 14960 states (over memory cap)
KLEE: WARNING: killing 14556 states (over memory cap)
KLEE: WARNING ONCE: calling external: __VERIFIER_nondet_u16_named(57434752) at /tmp/symbiotic-UJzJK_/linux-3.12-rc1.tar.xz-144_2a-drivers--media--usb--dvb-usb--dvb-usb-dib0700.ko-entry_point_false-unreach-call.cil.out.c:14559
KLEE: ERROR: /tmp/symbiotic-UJzJK_/linux-3.12-rc1.tar.xz-144_2a-drivers--media--usb--dvb-usb--dvb-usb-dib0700.ko-entry_point_false-unreach-call.cil.out.c:14557: failed external call: __VERIFIER_nondet_u16_named
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14761 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-UJzJK_/linux-3.12-rc1.tar.xz-144_2a-drivers--media--usb--dvb-usb--dvb-usb-dib0700.ko-entry_point_false-unreach-call.cil.out.c:14679: failed external call: __VERIFIER_nondet_u16_named
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14726 states (over memory cap)
KLEE: WARNING: killing 14693 states (over memory cap)
KLEE: WARNING: killing 14176 states (over memory cap)
KLEE: WARNING: killing 14503 states (over memory cap)
KLEE: WARNING: killing 14342 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-UJzJK_/linux-3.12-rc1.tar.xz-144_2a-drivers--media--usb--dvb-usb--dvb-usb-dib0700.ko-entry_point_false-unreach-call.cil.out.c:7240: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-UJzJK_/linux-3.12-rc1.tar.xz-144_2a-drivers--media--usb--dvb-usb--dvb-usb-dib0700.ko-entry_point_false-unreach-call.cil.out.c:7734: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15270 states (over memory cap)
KLEE: WARNING: killing 15230 states (over memory cap)
KLEE: WARNING: killing 15441 states (over memory cap)
KLEE: WARNING: killing 15650 states (over memory cap)
KLEE: WARNING: killing 15740 states (over memory cap)
KLEE: WARNING: killing 15714 states (over memory cap)
KLEE: WARNING: killing 15814 states (over memory cap)
KLEE: WARNING: killing 16019 states (over memory cap)
KLEE: WARNING: killing 16467 states (over memory cap)
KLEE: WARNING: killing 16330 states (over memory cap)
KLEE: WARNING: killing 16900 states (over memory cap)
KLEE: WARNING: killing 16639 states (over memory cap)
KLEE: WARNING: killing 16621 states (over memory cap)
KLEE: WARNING: killing 16714 states (over memory cap)
KLEE: WARNING: killing 17519 states (over memory cap)
KLEE: WARNING: killing 17377 states (over memory cap)
KLEE: WARNING: killing 17122 states (over memory cap)
KLEE: WARNING: killing 16870 states (over memory cap)
KLEE: WARNING: killing 16727 states (over memory cap)
KLEE: WARNING: killing 16240 states (over memory cap)
KLEE: WARNING: killing 16108 states (over memory cap)
KLEE: WARNING: killing 17363 states (over memory cap)
KLEE: WARNING: killing 15717 states (over memory cap)
KLEE: WARNING: killing 15810 states (over memory cap)
KLEE: WARNING: killing 15670 states (over memory cap)
KLEE: WARNING: killing 15065 states (over memory cap)
KLEE: WARNING: killing 15389 states (over memory cap)
KLEE: WARNING: killing 15478 states (over memory cap)
KLEE: WARNING: killing 15917 states (over memory cap)
KLEE: WARNING: killing 15431 states (over memory cap)
KLEE: WARNING: killing 15865 states (over memory cap)
KLEE: WARNING: killing 15609 states (over memory cap)
KLEE: WARNING: killing 15821 states (over memory cap)
KLEE: WARNING: killing 16254 states (over memory cap)
KLEE: WARNING: killing 16009 states (over memory cap)
KLEE: WARNING: killing 15873 states (over memory cap)
KLEE: WARNING: killing 15958 states (over memory cap)
KLEE: WARNING: killing 16164 states (over memory cap)
KLEE: WARNING: killing 16140 states (over memory cap)
KLEE: WARNING: killing 16009 states (over memory cap)
KLEE: WARNING: killing 16215 states (over memory cap)
KLEE: WARNING: killing 16423 states (over memory cap)
KLEE: WARNING: killing 15722 states (over memory cap)
KLEE: WARNING: killing 16158 states (over memory cap)
KLEE: WARNING: killing 16356 states (over memory cap)
KLEE: WARNING: killing 15441 states (over memory cap)
KLEE: WARNING: killing 15981 states (over memory cap)
KLEE: WARNING: killing 16073 states (over memory cap)
KLEE: WARNING: killing 16392 states (over memory cap)
KLEE: WARNING: killing 16481 states (over memory cap)
KLEE: WARNING: killing 15793 states (over memory cap)
KLEE: WARNING: killing 15773 states (over memory cap)
KLEE: WARNING: killing 15865 states (over memory cap)
KLEE: WARNING: killing 16627 states (over memory cap)
KLEE: WARNING: killing 16382 states (over memory cap)
KLEE: WARNING: killing 16141 states (over memory cap)
KLEE: WARNING: killing 16124 states (over memory cap)
KLEE: WARNING: killing 16545 states (over memory cap)
KLEE: WARNING: killing 16534 states (over memory cap)
KLEE: WARNING: killing 16405 states (over memory cap)
KLEE: WARNING: killing 15938 states (over memory cap)
KLEE: WARNING: killing 16037 states (over memory cap)
KLEE: WARNING: killing 16351 states (over memory cap)
KLEE: WARNING: killing 16550 states (over memory cap)
KLEE: WARNING: killing 15433 states (over memory cap)
KLEE: WARNING: killing 16621 states (over memory cap)
KLEE: WARNING: killing 16055 states (over memory cap)
KLEE: WARNING: killing 16032 states (over memory cap)
KLEE: WARNING: killing 16239 states (over memory cap)
KLEE: WARNING: killing 16109 states (over memory cap)
KLEE: WARNING: killing 16421 states (over memory cap)
KLEE: WARNING: killing 15743 states (over memory cap)
KLEE: WARNING: killing 16709 states (over memory cap)
KLEE: WARNING: killing 15816 states (over memory cap)
KLEE: WARNING: killing 16123 states (over memory cap)
KLEE: WARNING: killing 16438 states (over memory cap)
KLEE: WARNING: killing 15986 states (over memory cap)
KLEE: WARNING: killing 16180 states (over memory cap)
KLEE: WARNING: killing 16277 states (over memory cap)
KLEE: WARNING: killing 15712 states (over memory cap)
KLEE: WARNING: killing 16019 states (over memory cap)
KLEE: WARNING: killing 16435 states (over memory cap)
KLEE: WARNING: killing 16634 states (over memory cap)
KLEE: WARNING: killing 15973 states (over memory cap)
KLEE: WARNING: killing 16609 states (over memory cap)
KLEE: WARNING: killing 16593 states (over memory cap)
KLEE: WARNING: killing 16038 states (over memory cap)
KLEE: WARNING: killing 16875 states (over memory cap)
KLEE: WARNING: killing 16326 states (over memory cap)
KLEE: WARNING: killing 16088 states (over memory cap)
KLEE: WARNING: killing 15749 states (over memory cap)
KLEE: WARNING: killing 16380 states (over memory cap)
KLEE: WARNING: killing 16686 states (over memory cap)
KLEE: WARNING: killing 16348 states (over memory cap)
KLEE: WARNING: killing 16651 states (over memory cap)
KLEE: WARNING: killing 16525 states (over memory cap)
KLEE: WARNING: killing 15868 states (over memory cap)
KLEE: WARNING: killing 16387 states (over memory cap)
KLEE: WARNING: killing 16795 states (over memory cap)
KLEE: WARNING: killing 15711 states (over memory cap)
KLEE: WARNING: killing 15158 states (over memory cap)
KLEE: WARNING: killing 15892 states (over memory cap)
KLEE: WARNING: killing 16406 states (over memory cap)
KLEE: WARNING: killing 16276 states (over memory cap)
KLEE: WARNING: killing 16269 states (over memory cap)
KLEE: WARNING: killing 15821 states (over memory cap)
KLEE: WARNING: killing 15914 states (over memory cap)
KLEE: WARNING: killing 16325 states (over memory cap)
KLEE: WARNING: killing 16308 states (over memory cap)
KLEE: WARNING: killing 15976 states (over memory cap)
KLEE: WARNING: killing 16167 states (over memory cap)
KLEE: WARNING: killing 15946 states (over memory cap)
KLEE: WARNING: killing 15923 states (over memory cap)
KLEE: WARNING: killing 16115 states (over memory cap)
KLEE: WARNING: killing 16204 states (over memory cap)
KLEE: WARNING: killing 15666 states (over memory cap)
KLEE: WARNING: killing 16075 states (over memory cap)
KLEE: WARNING: killing 16061 states (over memory cap)
KLEE: WARNING: killing 15936 states (over memory cap)
KLEE: WARNING: killing 16026 states (over memory cap)
KLEE: WARNING: killing 16744 states (over memory cap)
KLEE: WARNING: killing 15584 states (over memory cap)
KLEE: WARNING: killing 16612 states (over memory cap)
KLEE: WARNING: killing 16077 states (over memory cap)
KLEE: WARNING: killing 15849 states (over memory cap)
KLEE: WARNING: killing 16152 states (over memory cap)
KLEE: WARNING: killing 16440 states (over memory cap)
KLEE: WARNING: killing 16325 states (over memory cap)
KLEE: WARNING: killing 15894 states (over memory cap)
KLEE: WARNING: killing 15880 states (over memory cap)
KLEE: WARNING: killing 17004 states (over memory cap)
KLEE: WARNING: killing 16882 states (over memory cap)
KLEE: WARNING: killing 16144 states (over memory cap)
KLEE: WARNING: killing 16126 states (over memory cap)
KLEE: WARNING: killing 16009 states (over memory cap)
KLEE: WARNING: killing 16612 states (over memory cap)
KLEE: WARNING: killing 15462 states (over memory cap)
KLEE: WARNING: killing 15962 states (over memory cap)
KLEE: WARNING: killing 16570 states (over memory cap)
KLEE: WARNING: killing 16244 states (over memory cap)
KLEE: WARNING: killing 15921 states (over memory cap)
KLEE: WARNING: killing 16008 states (over memory cap)
