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--net--wireless--rndis_wlan.ko-ldv_main0_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.: 201 159 1700 12595
Removed infinite loop in wiphy_priv
INFO: Compilation, preparation and instrumentation time: 0.555176019669
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'usbnet_pause_rx' (function is undefined)
Removed calls to 'usbnet_purge_paused_rxq' (function is undefined)
Removed calls to 'usbnet_resume_rx' (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 'netif_carrier_off' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'wiphy_free' (function is undefined)
Removed calls to 'rndis_unbind' (function is undefined)
Removed calls to 'wiphy_unregister' (function is undefined)
Removed calls to 'cfg80211_scan_done' (function is undefined)
Removed calls to 'cfg80211_michael_mic_failure' (function is undefined)
Removed calls to 'cfg80211_pmksa_candidate_notify' (function is undefined)
Defining function netdev_info as symbolic
Defining function queue_work as symbolic
Defining function sprintf as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Defining function rndis_command as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Defining function cancel_delayed_work_sync as symbolic
Defining function cancel_work_sync as symbolic
Defining function netdev_warn as symbolic
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Defining function round_jiffies_relative as symbolic
Defining function queue_delayed_work as symbolic
Defining function wiphy_new as symbolic
Defining function __alloc_workqueue_key as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'cfg80211_put_bss' (function is undefined)
Removed calls to 'cfg80211_connect_result' (function is undefined)
Removed calls to 'cfg80211_roamed' (function is undefined)
Removed calls to 'cfg80211_ibss_joined' (function is undefined)
Removed calls to 'netif_carrier_on' (function is undefined)
Removed calls to 'cfg80211_disconnected' (function is undefined)
Removed calls to 'cfg80211_cqm_rssi_notify' (function is undefined)
Defining function generic_rndis_bind as symbolic
Defining function wiphy_register as symbolic
Defining function cfg80211_inform_bss as symbolic
Defining function __ieee80211_get_channel as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function krealloc as symbolic
Defining function ieee80211_frequency_to_channel as symbolic
Defining function netdev_err as symbolic
Defining function usbnet_open as symbolic
Defining function usbnet_stop as symbolic
Defining function usbnet_start_xmit as symbolic
Defining function eth_mac_addr as symbolic
Defining function eth_validate_addr as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  strcmp
  strcpy
  strlen
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.503312110901
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 284 129 814 8361
INFO: Starting verification
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "rndis_connect" has inline asm
KLEE: WARNING ONCE: function "rndis_disconnect" has inline asm
KLEE: WARNING ONCE: function "rndis_change_virtual_intf" has inline asm
KLEE: WARNING ONCE: function "rndis_set_wiphy_params" has inline asm
KLEE: WARNING ONCE: function "rndis_set_tx_power" has inline asm
KLEE: WARNING ONCE: function "rndis_get_tx_power" has inline asm
KLEE: WARNING ONCE: function "rndis_join_ibss" has inline asm
KLEE: WARNING ONCE: function "rndis_leave_ibss" has inline asm
KLEE: WARNING ONCE: function "rndis_add_key" has inline asm
KLEE: WARNING ONCE: function "rndis_del_key" has inline asm
KLEE: WARNING ONCE: function "rndis_set_default_key" has inline asm
KLEE: WARNING ONCE: function "rndis_get_station" has inline asm
KLEE: WARNING ONCE: function "rndis_dump_station" has inline asm
KLEE: WARNING ONCE: function "rndis_set_pmksa" has inline asm
KLEE: WARNING ONCE: function "rndis_del_pmksa" has inline asm
KLEE: WARNING ONCE: function "rndis_flush_pmksa" has inline asm
KLEE: WARNING ONCE: function "rndis_set_power_mgmt" has inline asm
KLEE: WARNING ONCE: function "rndis_wlan_set_multicast_list" has inline asm
KLEE: WARNING ONCE: function "rndis_wlan_indication" has inline asm
KLEE: WARNING ONCE: function "rndis_wlan_worker" has inline asm
KLEE: WARNING ONCE: function "rndis_set_cqm_rssi_config" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to function: usbnet_tx_timeout
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6188: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6188: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6329: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:8454: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6188: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:8456: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9935: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9935: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9936: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9937: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6329: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:10803: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:10803: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:8466: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9448: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6188: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6188: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:10804: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6188: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6139: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6139: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6329: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6329: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9685: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:10523: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:10557: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YdlTLv/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:8539: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
