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-drivers--net--wireless--hostap--hostap.ko-main.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.: 473 388 5665 38580
INFO: Compilation, preparation and instrumentation time: 1.19273781776
Defining function strlcpy as symbolic
Defining function snprintf as symbolic
Defining function eth_header as symbolic
Defining function eth_rebuild_header as symbolic
Defining function eth_header_cache as symbolic
Removed calls to 'netif_carrier_on' (function is undefined)
Defining function iw_handler_set_spy as symbolic
Defining function iw_handler_get_spy as symbolic
Defining function iw_handler_set_thrspy as symbolic
Defining function iw_handler_get_thrspy as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to 'lib80211_crypt_delayed_deinit' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Defining function printk as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function schedule_work as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'wireless_send_event' (function is undefined)
Defining function skb_put as symbolic
Defining function dev_queue_xmit as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function lib80211_get_crypto_ops as symbolic
Defining function __request_module as symbolic
Defining function try_module_get as symbolic
Defining function sprintf as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Defining function schedule_timeout as symbolic
Defining function del_timer as symbolic
Removed calls to 'unregister_netdevice_queue' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Removed calls to 'rtnl_lock' (function is undefined)
Removed calls to 'rtnl_unlock' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Defining function alloc_etherdev_mqs as symbolic
Removed calls to 'ether_setup' (function is undefined)
Defining function register_netdevice as symbolic
Defining function default_wake_function as symbolic
Removed calls to 'netif_device_attach' (function is undefined)
Removed calls to 'netif_device_detach' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to '_raw_read_lock_bh' (function is undefined)
Removed calls to '_raw_read_unlock_bh' (function is undefined)
Defining function eth_validate_addr as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function capable as symbolic
Removed calls to '_raw_write_unlock_irqrestore' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function _copy_to_user as symbolic
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to 'skb_queue_purge' (function is undefined)
Defining function _copy_from_user as symbolic
Removed calls to '__const_udelay' (function is undefined)
Defining function _raw_write_lock_irqsave as symbolic
Defining function cancel_work_sync as symbolic
Defining function dev_close as symbolic
Defining function dev_open as symbolic
Removed calls to 'consume_skb' (function is undefined)
Removed calls to 'skb_queue_tail' (function is undefined)
Defining function net_ratelimit as symbolic
Defining function pskb_expand_head as symbolic
Defining function skb_copy as symbolic
Defining function skb_pull as symbolic
Defining function skb_realloc_headroom as symbolic
Defining function skb_push as symbolic
Removed calls to 'dev_kfree_skb_any' (function is undefined)
Defining function netif_rx as symbolic
Removed calls to 'wireless_spy_update' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'skb_trim' (function is undefined)
Defining function skb_clone as symbolic
Defining function eth_type_trans as symbolic
Removed calls to 'get_random_bytes' (function is undefined)
Defining function skb_dequeue as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Defining function create_proc_entry as symbolic
Defining function flush_work as symbolic
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to 'eth_header_cache_update' (function is undefined)
Defining function ldv_hostap_netdev_ops_ndo_init_3 as symbolic
Defining function ldv_hostap_netdev_ops_ndo_uninit_3 as symbolic
Defining function ldv_hostap_mgmt_netdev_ops_ndo_init_2 as symbolic
Defining function ldv_hostap_mgmt_netdev_ops_ndo_uninit_2 as symbolic
Defining function ldv_hostap_master_ops_ndo_init_1 as symbolic
Defining function ldv_hostap_master_ops_ndo_uninit_1 as symbolic
Defining function proc_mkdir as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strcpy
  strlen
  strncpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 1.09998393059
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 621 305 3077 20605
INFO: Starting verification
KLEE: WARNING ONCE: function "hostap_get_wireless_stats" has inline asm
KLEE: WARNING ONCE: function "prism2_ioctl_siwencodeext" has inline asm
KLEE: WARNING ONCE: function "prism2_ioctl_giwencodeext" has inline asm
KLEE: WARNING ONCE: function "ap_crypt_get_ptrs" has inline asm
KLEE: WARNING ONCE: function "ap_add_sta" has inline asm
KLEE: WARNING ONCE: function "prism2_ioctl_priv_prism2_param" has inline asm
KLEE: WARNING ONCE: function "prism2_open" has inline asm
KLEE: WARNING ONCE: function "hostap_ioctl" has inline asm
KLEE: WARNING ONCE: function "netif_stop_queue" has inline asm
KLEE: WARNING ONCE: function "prism2_hostapd" has inline asm
KLEE: WARNING ONCE: function "hostap_master_start_xmit" has inline asm
KLEE: WARNING ONCE: function "hostap_handle_sta_tx" has inline asm
KLEE: WARNING ONCE: function "hostap_handle_sta_release" has inline asm
KLEE: WARNING ONCE: function "hostap_80211_rx" has inline asm
KLEE: WARNING ONCE: function "hostap_handle_sta_crypto" has inline asm
KLEE: WARNING ONCE: function "hostap_rx_frame_decrypt" has inline asm
KLEE: WARNING ONCE: function "hostap_update_sta_ps" has inline asm
KLEE: WARNING ONCE: function "hostap_rx" has inline asm
KLEE: WARNING ONCE: function "hostap_handle_sta_rx" has inline asm
KLEE: WARNING ONCE: function "ap_handle_dropped_data" has inline asm
KLEE: WARNING ONCE: function "handle_assoc" has inline asm
KLEE: WARNING ONCE: function "handle_add_proc_queue" has inline asm
KLEE: WARNING ONCE: function "hostap_ap_tx_cb_auth" has inline asm
KLEE: WARNING ONCE: function "hostap_ap_tx_cb_assoc" has inline asm
KLEE: WARNING ONCE: function "hostap_info_process" has inline asm
KLEE: WARNING ONCE: function "handle_info_queue" has inline asm
KLEE: WARNING: undefined reference to function: eth_header_cache_update
KLEE: WARNING: undefined reference to function: free_netdev
KLEE: ERROR: /tmp/symbiotic-3Ib8Fj/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--net--wireless--hostap--hostap.ko-main.cil.out.c:13744: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3Ib8Fj/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--net--wireless--hostap--hostap.ko-main.cil.out.c:18351: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3Ib8Fj/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--net--wireless--hostap--hostap.ko-main.cil.out.c:20871: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3Ib8Fj/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--net--wireless--hostap--hostap.ko-main.cil.out.c:19751: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3Ib8Fj/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--net--wireless--hostap--hostap.ko-main.cil.out.c:20971: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3Ib8Fj/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--net--wireless--hostap--hostap.ko-main.cil.out.c:19851: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9346 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 13954 states (over memory cap)
KLEE: WARNING: killing 13505 states (over memory cap)
KLEE: WARNING: killing 14001 states (over memory cap)
KLEE: WARNING: killing 14027 states (over memory cap)
KLEE: WARNING: killing 12992 states (over memory cap)
KLEE: WARNING: killing 13149 states (over memory cap)
KLEE: WARNING: killing 13647 states (over memory cap)
KLEE: WARNING: killing 13946 states (over memory cap)
KLEE: WARNING: killing 14307 states (over memory cap)
KLEE: WARNING: killing 14481 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-3Ib8Fj/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--net--wireless--hostap--hostap.ko-main.cil.out.c:19676: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14516 states (over memory cap)
KLEE: WARNING: killing 14691 states (over memory cap)
KLEE: WARNING: killing 14926 states (over memory cap)
KLEE: WARNING: killing 15165 states (over memory cap)
KLEE: WARNING: killing 15602 states (over memory cap)
KLEE: WARNING: killing 15189 states (over memory cap)
KLEE: WARNING: killing 14515 states (over memory cap)
KLEE: WARNING: killing 15086 states (over memory cap)
KLEE: WARNING: killing 14606 states (over memory cap)
KLEE: WARNING: killing 13927 states (over memory cap)
KLEE: WARNING: killing 14296 states (over memory cap)
KLEE: WARNING: killing 13813 states (over memory cap)
KLEE: WARNING: killing 13854 states (over memory cap)
KLEE: WARNING: killing 14281 states (over memory cap)
KLEE: WARNING: killing 14120 states (over memory cap)
KLEE: WARNING: killing 14225 states (over memory cap)
KLEE: WARNING: killing 14651 states (over memory cap)
KLEE: WARNING: killing 14113 states (over memory cap)
KLEE: WARNING: killing 14221 states (over memory cap)
KLEE: WARNING: killing 14264 states (over memory cap)
KLEE: WARNING: killing 14045 states (over memory cap)
KLEE: WARNING: killing 14667 states (over memory cap)
KLEE: WARNING: killing 14642 states (over memory cap)
KLEE: WARNING: killing 14559 states (over memory cap)
KLEE: WARNING: killing 14473 states (over memory cap)
KLEE: WARNING: killing 13565 states (over memory cap)
KLEE: WARNING: killing 14431 states (over memory cap)
KLEE: WARNING: killing 14670 states (over memory cap)
KLEE: WARNING: killing 14079 states (over memory cap)
KLEE: WARNING: killing 13865 states (over memory cap)
KLEE: WARNING: killing 14290 states (over memory cap)
KLEE: WARNING: killing 14706 states (over memory cap)
KLEE: WARNING: killing 14560 states (over memory cap)
KLEE: WARNING: killing 13912 states (over memory cap)
KLEE: WARNING: killing 14461 states (over memory cap)
KLEE: WARNING: killing 14123 states (over memory cap)
KLEE: WARNING: killing 14414 states (over memory cap)
KLEE: WARNING: killing 14150 states (over memory cap)
KLEE: WARNING: killing 14379 states (over memory cap)
KLEE: WARNING: killing 14358 states (over memory cap)
KLEE: WARNING: killing 14339 states (over memory cap)
KLEE: WARNING: killing 14258 states (over memory cap)
KLEE: WARNING: killing 14300 states (over memory cap)
KLEE: WARNING: killing 14341 states (over memory cap)
KLEE: WARNING: killing 13827 states (over memory cap)
KLEE: WARNING: killing 14607 states (over memory cap)
KLEE: WARNING: killing 14776 states (over memory cap)
KLEE: WARNING: killing 13710 states (over memory cap)
KLEE: WARNING: killing 14306 states (over memory cap)
KLEE: WARNING: killing 14414 states (over memory cap)
KLEE: WARNING: killing 14333 states (over memory cap)
KLEE: WARNING: killing 14689 states (over memory cap)
KLEE: WARNING: killing 13931 states (over memory cap)
KLEE: WARNING: killing 14035 states (over memory cap)
KLEE: WARNING: killing 14629 states (over memory cap)
KLEE: WARNING: killing 14066 states (over memory cap)
KLEE: WARNING: killing 13741 states (over memory cap)
KLEE: WARNING: killing 14391 states (over memory cap)
KLEE: WARNING: killing 14433 states (over memory cap)
KLEE: WARNING: killing 14484 states (over memory cap)
KLEE: WARNING: killing 14342 states (over memory cap)
KLEE: WARNING: killing 14147 states (over memory cap)
KLEE: WARNING: killing 13947 states (over memory cap)
KLEE: WARNING: killing 14227 states (over memory cap)
KLEE: WARNING: killing 14815 states (over memory cap)
KLEE: WARNING: killing 13831 states (over memory cap)
KLEE: WARNING: killing 14415 states (over memory cap)
KLEE: WARNING: killing 14526 states (over memory cap)
KLEE: WARNING: killing 14629 states (over memory cap)
KLEE: WARNING: killing 13886 states (over memory cap)
KLEE: WARNING: killing 14350 states (over memory cap)
KLEE: WARNING: killing 14214 states (over memory cap)
KLEE: WARNING: killing 14497 states (over memory cap)
KLEE: WARNING: killing 13941 states (over memory cap)
KLEE: WARNING: killing 14460 states (over memory cap)
KLEE: WARNING: killing 14452 states (over memory cap)
KLEE: WARNING: killing 14736 states (over memory cap)
KLEE: WARNING: killing 14542 states (over memory cap)
KLEE: WARNING: killing 13932 states (over memory cap)
KLEE: WARNING: killing 13730 states (over memory cap)
KLEE: WARNING: killing 13773 states (over memory cap)
KLEE: WARNING: killing 13404 states (over memory cap)
KLEE: WARNING: killing 14390 states (over memory cap)
KLEE: WARNING: killing 14552 states (over memory cap)
KLEE: WARNING: killing 14424 states (over memory cap)
KLEE: WARNING: killing 13875 states (over memory cap)
KLEE: WARNING: killing 14275 states (over memory cap)
KLEE: WARNING: killing 14437 states (over memory cap)
KLEE: WARNING: killing 14189 states (over memory cap)
KLEE: WARNING: killing 14287 states (over memory cap)
KLEE: WARNING: killing 14449 states (over memory cap)
KLEE: WARNING: killing 14664 states (over memory cap)
KLEE: WARNING: killing 13885 states (over memory cap)
KLEE: WARNING: killing 14460 states (over memory cap)
KLEE: WARNING: killing 13974 states (over memory cap)
KLEE: WARNING: killing 13957 states (over memory cap)
KLEE: WARNING: killing 14061 states (over memory cap)
KLEE: WARNING: killing 14396 states (over memory cap)
KLEE: WARNING: killing 13911 states (over memory cap)
KLEE: WARNING: killing 14183 states (over memory cap)
KLEE: WARNING: killing 14168 states (over memory cap)
KLEE: WARNING: killing 14154 states (over memory cap)
KLEE: WARNING: killing 13682 states (over memory cap)
KLEE: WARNING: killing 14587 states (over memory cap)
KLEE: WARNING: killing 14691 states (over memory cap)
KLEE: WARNING: killing 14154 states (over memory cap)
KLEE: WARNING: killing 14319 states (over memory cap)
KLEE: WARNING: killing 14483 states (over memory cap)
KLEE: WARNING: killing 14410 states (over memory cap)
KLEE: WARNING: killing 14513 states (over memory cap)
KLEE: WARNING: killing 14098 states (over memory cap)
KLEE: WARNING: killing 13959 states (over memory cap)
KLEE: WARNING: killing 14519 states (over memory cap)
KLEE: WARNING: killing 13991 states (over memory cap)
KLEE: WARNING: killing 14376 states (over memory cap)
KLEE: WARNING: killing 14358 states (over memory cap)
KLEE: WARNING: killing 14179 states (over memory cap)
KLEE: WARNING: killing 14738 states (over memory cap)
KLEE: WARNING: killing 14091 states (over memory cap)
KLEE: WARNING: killing 14590 states (over memory cap)
KLEE: WARNING: killing 14059 states (over memory cap)
KLEE: WARNING: killing 13762 states (over memory cap)
KLEE: WARNING: killing 13863 states (over memory cap)
KLEE: WARNING: killing 13846 states (over memory cap)
KLEE: WARNING: killing 14225 states (over memory cap)
KLEE: WARNING: killing 14210 states (over memory cap)
KLEE: WARNING: killing 14537 states (over memory cap)
KLEE: WARNING: killing 14015 states (over memory cap)
KLEE: WARNING: killing 14732 states (over memory cap)
KLEE: WARNING: killing 13932 states (over memory cap)
KLEE: WARNING: killing 13972 states (over memory cap)
KLEE: WARNING: killing 14132 states (over memory cap)
KLEE: WARNING: killing 14168 states (over memory cap)
KLEE: WARNING: killing 13872 states (over memory cap)
KLEE: WARNING: killing 13860 states (over memory cap)
KLEE: WARNING: killing 14403 states (over memory cap)
KLEE: WARNING: killing 14846 states (over memory cap)
KLEE: WARNING: killing 14552 states (over memory cap)
KLEE: WARNING: killing 14091 states (over memory cap)
KLEE: WARNING: killing 14129 states (over memory cap)
KLEE: WARNING: killing 13721 states (over memory cap)
KLEE: WARNING: killing 14383 states (over memory cap)
KLEE: WARNING: killing 14648 states (over memory cap)
KLEE: WARNING: killing 14241 states (over memory cap)
KLEE: WARNING: killing 14621 states (over memory cap)
KLEE: WARNING: killing 14329 states (over memory cap)
KLEE: WARNING: killing 14093 states (over memory cap)
KLEE: WARNING: killing 13967 states (over memory cap)
KLEE: WARNING: killing 14062 states (over memory cap)
KLEE: WARNING: killing 14107 states (over memory cap)
