bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--rtlwifi--rtl8192cu--rtl8192cu.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.: 288 270 3524 27478
Removed infinite loop in arch_local_save_flags
Removed infinite loop in arch_local_irq_enable
Removed infinite loop in arch_local_irq_restore
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.853627920151
Removed calls to 'vfree' (function is undefined)
Removed calls to 'rtl_efuse_shadow_map_update' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'rtl_cam_reset_all_entry' (function is undefined)
Removed calls to 'rtl92c_phy_set_rfpath_switch' (function is undefined)
Removed calls to 'rtl92c_phy_iq_calibrate' (function is undefined)
Removed calls to 'rtl92c_dm_check_txpower_tracking' (function is undefined)
Removed calls to 'rtl92c_phy_lc_calibrate' (function is undefined)
Removed calls to 'rtl92c_dm_init' (function is undefined)
Removed calls to 'trace_hardirqs_off' (function is undefined)
Defining function rtl92c_phy_sw_chnl as symbolic
Removed calls to 'rtl92c_dm_init_edca_turbo' (function is undefined)
Removed calls to 'rtl92c_dm_rf_saving' (function is undefined)
Removed calls to 'rtl92c_set_fw_pwrmode_cmd' (function is undefined)
Removed calls to 'rtl92c_set_fw_rsvdpagepkt' (function is undefined)
Removed calls to 'rtl92c_set_fw_joinbss_report_cmd' (function is undefined)
Removed calls to 'rtl_get_tcb_desc' (function is undefined)
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'rtl92ce_phy_set_rf_on' (function is undefined)
Removed calls to '_rtl92c_phy_set_rf_sleep' (function is undefined)
Removed calls to 'rtl_cam_mark_invalid' (function is undefined)
Removed calls to 'rtl_cam_empty_entry' (function is undefined)
Removed calls to 'rtl_cam_del_entry' (function is undefined)
Defining function rtl92c_phy_query_bb_reg as symbolic
Removed calls to '_rtl92c_phy_rf_serial_write' (function is undefined)
Removed calls to '_rtl92c_phy_fw_rf_serial_write' (function is undefined)
Removed calls to 'rtl_addr_delay' (function is undefined)
Removed calls to '_rtl92c_store_pwrIndex_diffrate_offset' (function is undefined)
Removed calls to 'rtl92c_phy_set_txpower_level' (function is undefined)
Removed calls to 'dm_restorepowerindex' (function is undefined)
Removed calls to 'dm_writepowerindex' (function is undefined)
Defining function printk as symbolic
Removed calls to 'rtl_rfreg_delay' (function is undefined)
Defining function _rtl92c_phy_rf_serial_read as symbolic
Defining function _rtl92c_phy_calculate_bit_shift as symbolic
Defining function _rtl92c_phy_fw_rf_serial_read as symbolic
Defining function rtl_cam_get_free_entry as symbolic
Defining function rtl_cam_delete_one_entry as symbolic
Defining function rtl_cam_add_one_entry as symbolic
Defining function rtl_ps_enable_nic as symbolic
Defining function jiffies_to_msecs as symbolic
Defining function rtl_ps_disable_nic as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function rtlwifi_rate_mapping as symbolic
Removed calls to 'rtl_process_phyinfo' (function is undefined)
Defining function skb_push as symbolic
Defining function ieee80211_find_sta as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_watching as symbolic
Defining function queue_work_on as symbolic
Defining function rtl92c_phy_set_io_cmd as symbolic
Defining function rtl92c_download_fw as symbolic
Removed calls to '_rtl92c_phy_init_bb_rf_register_definition' (function is undefined)
Defining function rtl92c_phy_rf_config as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function efuse_read_1byte as symbolic
Defining function _rtl92c_phy_bb8192c_config_parafile as symbolic
Defining function vzalloc as symbolic
Defining function request_firmware_nowait as symbolic
Removed calls to 'ieee80211_rx' (function is undefined)
Defining function skb_pull as symbolic
Defining function rtl_usb_probe as symbolic
Removed calls to 'rtl_usb_disconnect' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Removed calls to 'rtl92c_phy_set_bb_reg' (function is undefined)
Removed calls to 'rtl92c_fill_h2c_cmd' (function is undefined)
Removed calls to 'rtl92c_phy_set_bw_mode' (function is undefined)
Removed calls to 'rtl92c_dm_watchdog' (function is undefined)
Removed calls to 'rtl_phy_scan_operation_backup' (function is undefined)
Defining function ldv_release_3 as symbolic
Defining function ldv_probe_3 as symbolic
Defining function usb_register_driver as symbolic
Linked our definitions to these undefined functions:
  __memcpy
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_u32_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.92897605896
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 386 207 2188 15517
INFO: Starting verification
KLEE: WARNING ONCE: function "rtl92cu_init_sw_vars" has inline asm
KLEE: WARNING ONCE: function "rtl92c_read_chip_version" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_read_eeprom_info" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_hw_init" has inline asm
KLEE: WARNING ONCE: function "rtl92c_set_qos" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_set_beacon_related_registers" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_set_beacon_interval" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_get_hw_reg" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_set_hw_reg" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_update_hal_rate_tbl" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_tx_fill_desc" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_tx_fill_cmddesc" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_gpio_radio_on_off_checking" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_phy_set_rf_power_state" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_led_control" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_enable_hw_security_config" has inline asm
KLEE: WARNING ONCE: function "rtl92c_set_key" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_phy_query_rf_reg" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_phy_set_rf_reg" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_phy_rf6052_config" has inline asm
KLEE: WARNING ONCE: function "_rtl92cu_phy_config_bb_with_headerfile" has inline asm
KLEE: WARNING ONCE: function "_rtl92cu_phy_config_bb_with_pgheaderfile" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_phy_set_bw_mode_callback" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_dm_dynamic_txpower" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_phy_rf6052_set_bandwidth" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_phy_config_rf_with_headerfile" has inline asm
KLEE: WARNING ONCE: function "_rtl92cu_set_media_status" has inline asm
KLEE: WARNING ONCE: function "_ResetDigitalProcedure1" has inline asm
KLEE: WARNING ONCE: function "rtl92c_set_network_type" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "_rtl92cu_phy_config_mac_with_headerfile" has inline asm
KLEE: WARNING ONCE: function "rtl92c_llt_write" has inline asm
KLEE: WARNING ONCE: function "rtl8192cu_rx_hdl" has inline asm
KLEE: WARNING ONCE: function "rtl8192cu_endpoint_mapping" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_sw_led_on" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_sw_led_off" has inline asm
KLEE: WARNING ONCE: function "rtl92c_set_mac_addr" has inline asm
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: rtl92c_dm_watchdog
KLEE: WARNING: undefined reference to function: rtl92c_fill_h2c_cmd
KLEE: WARNING: undefined reference to function: rtl92c_phy_set_bb_reg
KLEE: WARNING: undefined reference to function: rtl92c_phy_set_bw_mode
KLEE: WARNING: undefined reference to function: rtl_fw_cb
KLEE: WARNING: undefined reference to function: rtl_phy_scan_operation_backup
KLEE: WARNING: undefined reference to function: rtl_usb_disconnect
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-8FEfyZ/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "rtl92cu_init_sw_vars" has inline asm
KLEE: WARNING ONCE: function "rtl92c_read_chip_version" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_read_eeprom_info" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_hw_init" has inline asm
KLEE: WARNING ONCE: function "rtl92c_set_qos" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_set_beacon_related_registers" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_set_beacon_interval" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_get_hw_reg" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_set_hw_reg" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_update_hal_rate_tbl" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_tx_fill_desc" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_tx_fill_cmddesc" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_gpio_radio_on_off_checking" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_phy_set_rf_power_state" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_led_control" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_enable_hw_security_config" has inline asm
KLEE: WARNING ONCE: function "rtl92c_set_key" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_phy_query_rf_reg" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_phy_set_rf_reg" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_phy_rf6052_config" has inline asm
KLEE: WARNING ONCE: function "_rtl92cu_phy_config_bb_with_headerfile" has inline asm
KLEE: WARNING ONCE: function "_rtl92cu_phy_config_bb_with_pgheaderfile" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_phy_set_bw_mode_callback" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_dm_dynamic_txpower" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_phy_rf6052_set_bandwidth" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_phy_config_rf_with_headerfile" has inline asm
KLEE: WARNING ONCE: function "_rtl92cu_set_media_status" has inline asm
KLEE: WARNING ONCE: function "_ResetDigitalProcedure1" has inline asm
KLEE: WARNING ONCE: function "rtl92c_set_network_type" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "_rtl92cu_phy_config_mac_with_headerfile" has inline asm
KLEE: WARNING ONCE: function "rtl92c_llt_write" has inline asm
KLEE: WARNING ONCE: function "rtl8192cu_rx_hdl" has inline asm
KLEE: WARNING ONCE: function "rtl8192cu_endpoint_mapping" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_sw_led_on" has inline asm
KLEE: WARNING ONCE: function "rtl92cu_sw_led_off" has inline asm
KLEE: WARNING ONCE: function "rtl92c_set_mac_addr" has inline asm
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: rtl92c_dm_watchdog
KLEE: WARNING: undefined reference to function: rtl92c_fill_h2c_cmd
KLEE: WARNING: undefined reference to function: rtl92c_phy_set_bb_reg
KLEE: WARNING: undefined reference to function: rtl92c_phy_set_bw_mode
KLEE: WARNING: undefined reference to function: rtl_fw_cb
KLEE: WARNING: undefined reference to function: rtl_phy_scan_operation_backup
KLEE: WARNING: undefined reference to function: rtl_usb_disconnect
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 2.06706595421
