bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--staging--rtl8723au--r8723au.ko-entry_point_true-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.: 2246 2257 26823 171585
Removed infinite loop in wdev_priv
Removed infinite loop in wiphy_priv
Removed infinite loop in wdev_priv___0
Removed infinite loop in wiphy_priv___0
Removed infinite loop in wdev_priv___1
Removed infinite loop in wiphy_priv___1
Removed infinite loop in wdev_priv___2
Removed infinite loop in wiphy_priv___2
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 5.32677912712
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Defining function printk as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function jiffies_to_msecs as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Defining function usb_control_msg as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function __msecs_to_jiffies as symbolic
Defining function rtw_cfg80211_pwr_mgmt as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Defining function queue_work_on as symbolic
Defining function get_my_bssid23a as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'netif_wake_subqueue' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function usb_submit_urb as symbolic
Removed calls to '__tasklet_hi_schedule' (function is undefined)
Removed calls to 'down' (function is undefined)
Removed calls to 'up' (function is undefined)
Defining function mod_timer as symbolic
Removed calls to '__udelay' (function is undefined)
Removed calls to 'usb_kill_urb' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function find_vpid as symbolic
Defining function kill_pid as symbolic
Defining function rtw_get_oper_ch23a as symbolic
Removed calls to 'netif_carrier_on' (function is undefined)
Defining function del_timer_sync as symbolic
Removed calls to 'cfg80211_roamed' (function is undefined)
Removed calls to 'cfg80211_connect_result' (function is undefined)
Defining function ieee80211_channel_to_frequency as symbolic
Defining function __ieee80211_get_channel as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'ieee80211_amsdu_to_8023s' (function is undefined)
Defining function skb_pull as symbolic
Defining function eth_type_trans as symbolic
Defining function netif_rx as symbolic
Defining function skb_clone as symbolic
Defining function cfg80211_find_ie as symbolic
Defining function wait_for_completion_timeout as symbolic
Removed calls to 'netif_tx_stop_all_queues' (function is undefined)
Removed calls to 'tasklet_kill' (function is undefined)
Removed calls to 'netif_tx_wake_queue' (function is undefined)
Defining function cfg80211_find_vendor_ie as symbolic
Removed calls to 'yield' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function skb_dequeue as symbolic
Removed calls to 'skb_queue_tail' (function is undefined)
Removed calls to '__tasklet_schedule' (function is undefined)
Defining function skb_put as symbolic
Defining function __netdev_alloc_skb as symbolic
Removed calls to 'release_firmware' (function is undefined)
Defining function request_firmware as symbolic
Defining function kmemdup as symbolic
Removed calls to 'cfg80211_disconnected' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to 'cfg80211_scan_done' (function is undefined)
Defining function cfg80211_rx_mgmt as symbolic
Removed calls to 'cfg80211_put_bss' (function is undefined)
Defining function cfg80211_inform_bss_width as symbolic
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'unregister_netdevice_queue' (function is undefined)
Removed calls to 'cfg80211_mgmt_tx_status' (function is undefined)
Defining function ieee80211_frequency_to_channel as symbolic
Defining function rtw_is_scan_deny as symbolic
Defining function alloc_etherdev_mqs as symbolic
Defining function register_netdevice as symbolic
Removed calls to 'consume_skb' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Removed calls to 'netif_device_attach' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Removed calls to 'usb_autopm_put_interface' (function is undefined)
Removed calls to 'mutex_destroy' (function is undefined)
Removed calls to 'usb_put_dev' (function is undefined)
Defining function usb_reset_device as symbolic
Removed calls to 'wiphy_unregister' (function is undefined)
Removed calls to 'wiphy_free' (function is undefined)
Removed calls to 'usb_free_urb' (function is undefined)
Removed calls to 'skb_queue_purge' (function is undefined)
Defining function cancel_work_sync as symbolic
Defining function register_netdev as symbolic
Defining function dev_alloc_name as symbolic
Defining function device_init_wakeup as symbolic
Defining function usb_autopm_get_interface as symbolic
Removed calls to 'tasklet_init' (function is undefined)
Defining function usb_alloc_urb as symbolic
Removed calls to 'skb_trim' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'cfg80211_michael_mic_failure' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function wiphy_register as symbolic
Defining function wiphy_new_nm as symbolic
Defining function snprintf as symbolic
Defining function usb_get_dev as symbolic
Defining function queue_delayed_work_on as symbolic
Defining function mutex_trylock as symbolic
Defining function rtw_set_ie23a_ch_switch as symbolic
Defining function hal_ch_offset_to_secondary_ch_offset23a as symbolic
Defining function rtw_set_ie23a_secondary_ch_offset as symbolic
Defining function ldv_release_16 as symbolic
Defining function ldv_bind_16 as symbolic
Defining function ldv_ndo_init_17 as symbolic
Defining function ldv_ndo_uninit_17 as symbolic
Defining function ldv_ndo_init_15 as symbolic
Defining function ldv_ndo_uninit_15 as symbolic
Removed calls to 'ldv_initialize' (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:
  memcmp
  strncpy
  __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: 5.66537499428
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 2610 1787 16092 99573
INFO: Starting verification
KLEE: WARNING ONCE: function "sitesurvey_cmd_hdl23a" has inline asm
KLEE: WARNING ONCE: function "tasklet_hi_schedule" has inline asm
KLEE: WARNING ONCE: function "report_del_sta_event23a" has inline asm
KLEE: WARNING ONCE: function "report_join_res23a" has inline asm
KLEE: WARNING ONCE: function "usb_read_port_complete" has inline asm
KLEE: WARNING ONCE: function "wdev_priv" has inline asm
KLEE: WARNING ONCE: function "report_surveydone_event23a" has inline asm
KLEE: WARNING ONCE: function "report_survey_event23a" has inline asm
KLEE: WARNING ONCE: function "report_add_sta_event23a" has inline asm
KLEE: WARNING ONCE: function "wdev_priv___1" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_add_virtual_intf" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_del_virtual_intf" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_change_iface" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_add_key" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_start_ap" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_change_beacon" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_get_station" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_scan" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_connect" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_disconnect" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_set_pmksa" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_del_pmksa" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_flush_pmksa" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_mgmt_tx" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_set_power_mgmt" has inline asm
KLEE: WARNING ONCE: function "rtw_xmit23a_entry23a" has inline asm
KLEE: WARNING ONCE: function "netdev_open23a" has inline asm
KLEE: WARNING ONCE: function "rtw_suspend" has inline asm
KLEE: WARNING ONCE: function "rtw_resume" has inline asm
KLEE: WARNING ONCE: function "rtw_wdev_unregister" has inline asm
KLEE: WARNING ONCE: function "rtl8723a_readefuse" has inline asm
KLEE: WARNING ONCE: function "Efuse_CalculateWordCnts23a" has inline asm
KLEE: WARNING ONCE: function "rtl8723a_EfuseGetCurrentSize_WiFi" has inline asm
KLEE: WARNING ONCE: function "rtl8723a_EfuseGetCurrentSize_BT" has inline asm
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-kjv4ZK/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "sitesurvey_cmd_hdl23a" has inline asm
KLEE: WARNING ONCE: function "tasklet_hi_schedule" has inline asm
KLEE: WARNING ONCE: function "report_del_sta_event23a" has inline asm
KLEE: WARNING ONCE: function "report_join_res23a" has inline asm
KLEE: WARNING ONCE: function "usb_read_port_complete" has inline asm
KLEE: WARNING ONCE: function "wdev_priv" has inline asm
KLEE: WARNING ONCE: function "report_surveydone_event23a" has inline asm
KLEE: WARNING ONCE: function "report_survey_event23a" has inline asm
KLEE: WARNING ONCE: function "report_add_sta_event23a" has inline asm
KLEE: WARNING ONCE: function "wdev_priv___1" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_add_virtual_intf" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_del_virtual_intf" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_change_iface" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_add_key" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_start_ap" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_change_beacon" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_get_station" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_scan" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_connect" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_disconnect" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_set_pmksa" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_del_pmksa" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_flush_pmksa" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_mgmt_tx" has inline asm
KLEE: WARNING ONCE: function "cfg80211_rtw_set_power_mgmt" has inline asm
KLEE: WARNING ONCE: function "rtw_xmit23a_entry23a" has inline asm
KLEE: WARNING ONCE: function "netdev_open23a" has inline asm
KLEE: WARNING ONCE: function "rtw_suspend" has inline asm
KLEE: WARNING ONCE: function "rtw_resume" has inline asm
KLEE: WARNING ONCE: function "rtw_wdev_unregister" has inline asm
KLEE: WARNING ONCE: function "rtl8723a_readefuse" has inline asm
KLEE: WARNING ONCE: function "Efuse_CalculateWordCnts23a" has inline asm
KLEE: WARNING ONCE: function "rtl8723a_EfuseGetCurrentSize_WiFi" has inline asm
KLEE: WARNING ONCE: function "rtl8723a_EfuseGetCurrentSize_BT" has inline asm
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: 12.4624488354
