bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--rtl8192e--rtl8192e--r8192e_pci.ko-ldv_main7_sequence_infinite_withcheck_stateful.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.: 640 587 7056 52903
Removed infinite loop in arch_local_save_flags
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_map_single_attrs___0
Removed infinite loop in dma_map_single_attrs
INFO: Compilation, preparation and instrumentation time: 1.76537179947
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'tasklet_init' (function is undefined)
Removed calls to 'dot11d_init' (function is undefined)
Removed calls to 'Dot11d_Channelmap' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to 'free_rtllib' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'netif_device_detach' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'pci_restore_state' (function is undefined)
Removed calls to 'netif_device_attach' (function is undefined)
Defining function printk as symbolic
Defining function pci_set_power_state as symbolic
Defining function pci_enable_device as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function rtllib_MgntDisconnect as symbolic
Defining function queue_delayed_work as symbolic
Removed calls to 'rtllib_softmac_stop_protocol' (function is undefined)
Defining function cancel_delayed_work as symbolic
Defining function cancel_work_sync as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function mod_timer as symbolic
Defining function __pci_enable_wake as symbolic
Defining function pci_bus_write_config_dword as symbolic
Defining function pci_bus_read_config_dword as symbolic
Defining function dev_get_drvdata as symbolic
Defining function del_timer_sync as symbolic
Defining function pci_save_state as symbolic
Defining function pci_choose_state as symbolic
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Removed calls to 'rtllib_sta_ps_send_null_frame' (function is undefined)
Defining function alloc_rtllib as symbolic
Defining function __request_region as symbolic
Defining function ioremap_nocache as symbolic
Defining function dev_alloc_name as symbolic
Defining function register_netdev as symbolic
Defining function create_proc_entry as symbolic
Defining function snprintf as symbolic
Removed calls to 'down' (function is undefined)
Removed calls to 'up' (function is undefined)
Removed calls to 'rtllib_ps_tx_ack' (function is undefined)
Removed calls to '__tasklet_schedule' (function is undefined)
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Defining function __phys_addr as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function request_threaded_irq as symbolic
Defining function call_usermodehelper_fns as symbolic
Removed calls to 'add_timer' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Removed calls to 'RemovePeerTS' (function is undefined)
Removed calls to 'notify_wx_assoc_event' (function is undefined)
Removed calls to 'rtllib_stop_scan_syncro' (function is undefined)
Removed calls to 'rtllib_stop_send_beacons' (function is undefined)
Removed calls to 'rtllib_stop_scan' (function is undefined)
Removed calls to 'rtllib_start_send_beacons' (function is undefined)
Removed calls to 'netif_carrier_on' (function is undefined)
Removed calls to 'HT_update_self_and_peer_setting' (function is undefined)
Removed calls to 'skb_trim' (function is undefined)
Removed calls to 'dev_kfree_skb_any' (function is undefined)
Defining function rtllib_get_beacon as symbolic
Defining function skb_push as symbolic
Defining function skb_dequeue as symbolic
Defining function skb_put as symbolic
Defining function rtllib_rx as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function rtllib_act_scanning as symbolic
Removed calls to 'rtllib_softmac_start_protocol' (function is undefined)
Removed calls to 'rtllib_reset_queue' (function is undefined)
Removed calls to '__netif_schedule' (function is undefined)
Defining function queue_work as symbolic
Defining function netpoll_trap as symbolic
Defining function vzalloc as symbolic
Removed calls to 'msleep' (function is undefined)
Defining function rtllib_legal_channel as symbolic
Defining function pcie_capability_read_word as symbolic
Defining function pci_bus_write_config_byte as symbolic
Defining function pci_bus_read_config_word as symbolic
Defining function pci_bus_read_config_byte as symbolic
Defining function dev_set_drvdata as symbolic
Defining function dma_supported as symbolic
Defining function dma_set_mask as symbolic
Removed calls to 'skb_queue_purge' (function is undefined)
Removed calls to 'release_firmware' (function is undefined)
Removed calls to 'skb_queue_tail' (function is undefined)
Defining function request_firmware as symbolic
Defining function rtllib_xmit as symbolic
Defining function eth_validate_addr as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function eth_change_mtu as symbolic
Defining function schedule_work as symbolic
Defining function rtllib_wpa_supplicant_ioctl as symbolic
Defining function _copy_from_user as symbolic
Removed calls to 'rtllib_start_scan_syncro' (function is undefined)
Defining function rtllib_wx_set_encode_ext as symbolic
Defining function rtllib_wx_set_auth as symbolic
Defining function rtllib_wx_set_gen_ie as symbolic
Defining function rtllib_wx_get_power as symbolic
Defining function rtllib_wx_set_power as symbolic
Defining function rtllib_wx_get_encode as symbolic
Defining function rtllib_wx_set_encode as symbolic
Defining function rtllib_wx_get_rts as symbolic
Defining function rtllib_wx_set_rts as symbolic
Defining function rtllib_wx_get_rate as symbolic
Defining function rtllib_wx_set_rate as symbolic
Defining function rtllib_wx_get_essid as symbolic
Defining function rtllib_wx_set_essid as symbolic
Defining function rtllib_wx_get_scan as symbolic
Defining function rtllib_wx_set_scan as symbolic
Defining function rtllib_wx_set_mlme as symbolic
Defining function rtllib_wx_get_wap as symbolic
Defining function rtllib_wx_set_wap as symbolic
Defining function rtllib_wx_get_mode as symbolic
Defining function rtllib_wx_set_mode as symbolic
Defining function rtllib_wx_get_freq as symbolic
Defining function rtllib_wx_set_freq as symbolic
Defining function rtllib_wx_get_name as symbolic
Removed calls to 'rtllib_EnableIntelPromiscuousMode' (function is undefined)
Removed calls to 'rtllib_DisableIntelPromiscuousMode' (function is undefined)
Defining function rtllib_wx_set_rawtx as symbolic
Defining function mutex_trylock as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'ldv_check_return_value_probe' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function __pci_register_driver as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strcpy
  strlen
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 1.74913597107
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 755 492 4138 29815
INFO: Starting verification
KLEE: WARNING ONCE: function "rtl8192E_suspend" has inline asm
KLEE: WARNING ONCE: function "SetRFPowerState" has inline asm
KLEE: WARNING ONCE: function "rtl8192_setBBreg" has inline asm
KLEE: WARNING ONCE: function "PHY_SetRtl8192eRfOff" has inline asm
KLEE: WARNING ONCE: function "rtl8192_down" has inline asm
KLEE: WARNING ONCE: function "pci_unmap_single" has inline asm
KLEE: WARNING ONCE: function "pci_free_consistent" has inline asm
KLEE: WARNING ONCE: function "netif_stop_queue" has inline asm
KLEE: WARNING ONCE: function "rtl8192_SetBWMode" has inline asm
KLEE: WARNING ONCE: function "rtl8192e_start_beacon" has inline asm
KLEE: WARNING ONCE: function "rtl8192e_SetHwReg" has inline asm
KLEE: WARNING ONCE: function "rtl8192_AllowAllDestAddr" has inline asm
KLEE: WARNING ONCE: function "InitialGain819xPci" has inline asm
KLEE: WARNING ONCE: function "rtl819x_watchdog_wqcallback" has inline asm
KLEE: WARNING ONCE: function "dm_txpower_trackingcallback" has inline asm
KLEE: WARNING ONCE: function "dm_rf_pathcheck_workitemcallback" has inline asm
KLEE: WARNING ONCE: function "rtl8192_interrupt_rsl" has inline asm
KLEE: WARNING ONCE: function "proc_get_registers_0" has inline asm
KLEE: WARNING ONCE: function "proc_get_registers_1" has inline asm
KLEE: WARNING ONCE: function "proc_get_registers_2" has inline asm
KLEE: WARNING ONCE: function "proc_get_registers_3" has inline asm
KLEE: WARNING ONCE: function "proc_get_registers_4" has inline asm
KLEE: WARNING ONCE: function "proc_get_registers_5" has inline asm
KLEE: WARNING ONCE: function "proc_get_registers_6" has inline asm
KLEE: WARNING ONCE: function "proc_get_registers_7" has inline asm
KLEE: WARNING ONCE: function "proc_get_registers_8" has inline asm
KLEE: WARNING ONCE: function "proc_get_registers_9" has inline asm
KLEE: WARNING ONCE: function "proc_get_registers_a" has inline asm
KLEE: WARNING ONCE: function "proc_get_registers_b" has inline asm
KLEE: WARNING ONCE: function "proc_get_registers_c" has inline asm
KLEE: WARNING ONCE: function "proc_get_registers_d" has inline asm
KLEE: WARNING ONCE: function "proc_get_registers_e" has inline asm
KLEE: WARNING ONCE: function "proc_get_cam_register_1" has inline asm
KLEE: WARNING ONCE: function "proc_get_cam_register_2" has inline asm
KLEE: WARNING ONCE: function "proc_get_cam_register_3" has inline asm
KLEE: WARNING ONCE: function "phy_FwRFSerialRead" has inline asm
KLEE: WARNING ONCE: function "rtl8192_phy_RFSerialRead" has inline asm
KLEE: WARNING ONCE: function "rtl8192_tx_isr" has inline asm
KLEE: WARNING ONCE: function "dm_fsync_timer_callback" has inline asm
KLEE: WARNING ONCE: function "dm_CheckRfCtrlGPIO" has inline asm
KLEE: WARNING ONCE: function "dm_cck_txpower_adjust" has inline asm
KLEE: WARNING ONCE: function "cmpk_message_handle_tx" has inline asm
KLEE: WARNING ONCE: function "hal_dm_watchdog" has inline asm
KLEE: WARNING ONCE: function "dm_backup_dynamic_mechanism_state" has inline asm
KLEE: WARNING ONCE: function "_rtl8192_up" has inline asm
KLEE: WARNING ONCE: function "EnableHWSecurityConfig8192" has inline asm
KLEE: WARNING ONCE: function "dm_restore_dynamic_mechanism_state" has inline asm
KLEE: WARNING ONCE: function "setKey" has inline asm
KLEE: WARNING ONCE: function "dm_ctrl_initgain_byrssi_highpwr" has inline asm
KLEE: WARNING ONCE: function "dm_check_fsync" has inline asm
KLEE: WARNING ONCE: function "dm_StartHWFsync" has inline asm
KLEE: WARNING ONCE: function "dm_EndSWFsync" has inline asm
KLEE: WARNING ONCE: function "dm_StartSWFsync" has inline asm
KLEE: WARNING ONCE: function "dm_EndHWFsync" has inline asm
KLEE: WARNING ONCE: function "phy_FwRFSerialWrite" has inline asm
KLEE: WARNING ONCE: function "rtl8192_phy_RFSerialWrite" has inline asm
KLEE: WARNING ONCE: function "rtl8192_SwChnl_WorkItem" has inline asm
KLEE: WARNING ONCE: function "rtl8192_SetBWModeWorkItem" has inline asm
KLEE: WARNING ONCE: function "rtl8192_tx" has inline asm
KLEE: WARNING ONCE: function "rtl8192_get_eeprom_size" has inline asm
KLEE: WARNING ONCE: function "rtl8192_adapter_start" has inline asm
KLEE: WARNING ONCE: function "rtl8192_link_change" has inline asm
KLEE: WARNING ONCE: function "rtl8192_rx_query_status_desc" has inline asm
KLEE: WARNING ONCE: function "rtl8192_halt_adapter" has inline asm
KLEE: WARNING ONCE: function "rtl8192_update_ratr_table" has inline asm
KLEE: WARNING ONCE: function "rtl8192_EnableInterrupt" has inline asm
KLEE: WARNING ONCE: function "rtl8192_DisableInterrupt" has inline asm
KLEE: WARNING ONCE: function "rtl8192_ClearInterrupt" has inline asm
KLEE: WARNING ONCE: function "rtl8192_enable_rx" has inline asm
KLEE: WARNING ONCE: function "rtl8192_enable_tx" has inline asm
KLEE: WARNING ONCE: function "rtl8192_interrupt_recognized" has inline asm
KLEE: WARNING ONCE: function "rtl8192_HalTxCheckStuck" has inline asm
KLEE: WARNING ONCE: function "rtl8192_HalRxCheckStuck" has inline asm
KLEE: WARNING ONCE: function "rtl8192_BBConfig" has inline asm
KLEE: WARNING ONCE: function "rtl8192_phy_getTxPower" has inline asm
KLEE: WARNING ONCE: function "init_firmware" has inline asm
KLEE: WARNING ONCE: function "phy_RF8256_Config_ParaFile" has inline asm
KLEE: WARNING ONCE: function "rtl8192_phy_checkBBAndRF" has inline asm
KLEE: WARNING ONCE: function "rtl8192_phyConfigBB" has inline asm
KLEE: WARNING ONCE: function "eprom_read" has inline asm
KLEE: WARNING ONCE: function "eprom_ck_cycle" has inline asm
KLEE: WARNING ONCE: function "eprom_w" has inline asm
KLEE: WARNING ONCE: function "rtl8192_ioctl" has inline asm
KLEE: WARNING ONCE: function "r8192_wx_set_enc" has inline asm
KLEE: WARNING ONCE: function "r8192_wx_set_enc_ext" has inline asm
KLEE: WARNING ONCE: function "write_nic_byte" has inline asm
KLEE: WARNING ONCE: function "read_nic_dword" has inline asm
KLEE: WARNING ONCE: function "write_nic_dword" has inline asm
KLEE: WARNING ONCE: function "CamResetAllEntry" has inline asm
KLEE: WARNING ONCE: function "rtl8192_QueryBBReg" has inline asm
KLEE: WARNING ONCE: function "read_nic_byte" has inline asm
KLEE: WARNING ONCE: function "rtl8192_irq_rx_tasklet" has inline asm
KLEE: WARNING ONCE: function "read_nic_word" has inline asm
KLEE: WARNING ONCE: function "write_nic_word" has inline asm
KLEE: WARNING ONCE: function "write_cam" has inline asm
KLEE: WARNING ONCE: function "read_cam" has inline asm
KLEE: WARNING ONCE: function "CAM_read_entry" has inline asm
KLEE: WARNING ONCE: function "write_nic_io_byte" has inline asm
KLEE: WARNING ONCE: function "read_nic_io_byte" has inline asm
KLEE: WARNING ONCE: function "write_nic_io_word" has inline asm
KLEE: WARNING ONCE: function "write_nic_io_dword" has inline asm
KLEE: WARNING ONCE: function "read_nic_io_word" has inline asm
KLEE: WARNING ONCE: function "read_nic_io_dword" has inline asm
KLEE: WARNING ONCE: function "dm_shadow_init" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING ONCE: flushing 43012 bytes on read, may be slow and/or crash: MO23[43012] allocated at global:Rtl8192PciEFwMainArray
KLEE: ERROR: /tmp/symbiotic-67t9to/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--rtl8192e--rtl8192e--r8192e_pci.ko-ldv_main7_sequence_infinite_withcheck_stateful.cil.out.c:31019: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-67t9to/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--rtl8192e--rtl8192e--r8192e_pci.ko-ldv_main7_sequence_infinite_withcheck_stateful.cil.out.c:30929: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-67t9to/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--rtl8192e--rtl8192e--r8192e_pci.ko-ldv_main7_sequence_infinite_withcheck_stateful.cil.out.c:31020: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-67t9to/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--rtl8192e--rtl8192e--r8192e_pci.ko-ldv_main7_sequence_infinite_withcheck_stateful.cil.out.c:28500: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-67t9to/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--rtl8192e--rtl8192e--r8192e_pci.ko-ldv_main7_sequence_infinite_withcheck_stateful.cil.out.c:31497: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-67t9to/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--rtl8192e--rtl8192e--r8192e_pci.ko-ldv_main7_sequence_infinite_withcheck_stateful.cil.out.c:31039: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-67t9to/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--rtl8192e--rtl8192e--r8192e_pci.ko-ldv_main7_sequence_infinite_withcheck_stateful.cil.out.c:31081: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-67t9to/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--rtl8192e--rtl8192e--r8192e_pci.ko-ldv_main7_sequence_infinite_withcheck_stateful.cil.out.c:31104: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-67t9to/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--rtl8192e--rtl8192e--r8192e_pci.ko-ldv_main7_sequence_infinite_withcheck_stateful.cil.out.c:31104: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: ERROR: concretized symbolic size to 2^17,analysis may be unsound
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: (location information missing) memory error: object read only
KLEE: NOTE: now ignoring this error at this location
