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--net--wireless--rndis_wlan.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.: 273 240 2663 15821
Removed infinite loop in wiphy_priv
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.636790037155
Removed calls to 'netdev_warn' (function is undefined)
Removed calls to 'netdev_err' (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_lock' (function is undefined)
Defining function rndis_command as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Defining function krealloc as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Defining function ieee80211_frequency_to_channel as symbolic
Defining function ieee80211_channel_to_frequency as symbolic
Removed calls to 'cfg80211_put_bss' (function is undefined)
Defining function queue_delayed_work_on as symbolic
Defining function cfg80211_inform_bss_width as symbolic
Defining function __ieee80211_get_channel 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 queue_work_on as symbolic
Defining function usbnet_probe as symbolic
Defining function usbnet_suspend as symbolic
Defining function usbnet_resume as symbolic
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)
Defining function rndis_rx_fixup as symbolic
Defining function rndis_tx_fixup as symbolic
Removed calls to 'netdev_info' (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 sprintf as symbolic
Defining function cancel_work_sync as symbolic
Defining function cancel_delayed_work_sync 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 __alloc_workqueue_key as symbolic
Removed calls to 'warn_slowpath_null' (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 __msecs_to_jiffies as symbolic
Defining function wiphy_new_nm as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'rndis_status' (function is undefined)
Removed calls to 'usbnet_tx_timeout' (function is undefined)
Removed calls to 'usbnet_disconnect' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Defining function ldv_disconnect_6 as symbolic
Defining function ldv_init_6 as symbolic
Defining function ldv_start_6 as symbolic
Defining function ldv_disconnect_7 as symbolic
Defining function ldv_init_7 as symbolic
Defining function ldv_start_7 as symbolic
Defining function ldv_release_9 as symbolic
Defining function ldv_bind_9 as symbolic
Defining function ldv_ndo_init_8 as symbolic
Defining function ldv_ndo_uninit_8 as symbolic
Defining function ldv_reset_resume_4 as symbolic
Defining function ldv_disconnect_5 as symbolic
Defining function ldv_init_5 as symbolic
Defining function ldv_start_5 as symbolic
Defining function usb_register_driver as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  strcmp
  strcpy
  strlen
  __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: 0.642781019211
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 305 225 1343 10647
INFO: Starting verification
KLEE: WARNING ONCE: function "rndis_change_virtual_intf" 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_connect" has inline asm
KLEE: WARNING ONCE: function "rndis_disconnect" 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_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_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_set_cqm_rssi_config" 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 "main" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to function: rndis_status
KLEE: WARNING: undefined reference to function: usbnet_disconnect
KLEE: WARNING: undefined reference to function: usbnet_tx_timeout
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_229cc89a-3fb5-41c7-aee6-df41d9e33d5a/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8461 states (over memory cap)
KLEE: WARNING: killing 12281 states (over memory cap)
KLEE: WARNING: killing 11528 states (over memory cap)
KLEE: WARNING: killing 12279 states (over memory cap)
KLEE: WARNING: killing 11889 states (over memory cap)
KLEE: WARNING: killing 11971 states (over memory cap)
KLEE: WARNING: killing 11945 states (over memory cap)
KLEE: WARNING: killing 12334 states (over memory cap)
KLEE: WARNING: killing 13036 states (over memory cap)
KLEE: WARNING: killing 12502 states (over memory cap)
KLEE: WARNING: killing 12790 states (over memory cap)
KLEE: WARNING: killing 13385 states (over memory cap)
KLEE: WARNING: killing 12707 states (over memory cap)
KLEE: WARNING: killing 13453 states (over memory cap)
KLEE: WARNING: killing 13031 states (over memory cap)
KLEE: WARNING: killing 12401 states (over memory cap)
KLEE: WARNING: killing 13196 states (over memory cap)
KLEE: WARNING: killing 13024 states (over memory cap)
KLEE: WARNING: killing 13263 states (over memory cap)
KLEE: WARNING: killing 12541 states (over memory cap)
KLEE: WARNING: killing 12674 states (over memory cap)
KLEE: WARNING: killing 13264 states (over memory cap)
KLEE: WARNING: killing 12693 states (over memory cap)
KLEE: WARNING: killing 12174 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 12510 states (over memory cap)
KLEE: WARNING: killing 12992 states (over memory cap)
KLEE: WARNING: killing 12627 states (over memory cap)
KLEE: WARNING: killing 12708 states (over memory cap)
KLEE: WARNING: killing 12995 states (over memory cap)
KLEE: WARNING: killing 12777 states (over memory cap)
KLEE: WARNING: killing 12764 states (over memory cap)
KLEE: WARNING: killing 12701 states (over memory cap)
KLEE: WARNING: killing 12934 states (over memory cap)
KLEE: WARNING: killing 13020 states (over memory cap)
KLEE: WARNING: killing 13207 states (over memory cap)
KLEE: WARNING: killing 12749 states (over memory cap)
KLEE: WARNING: killing 12584 states (over memory cap)
KLEE: WARNING: killing 12966 states (over memory cap)
KLEE: WARNING: killing 12753 states (over memory cap)
KLEE: WARNING: killing 12990 states (over memory cap)
KLEE: WARNING: killing 12830 states (over memory cap)
KLEE: WARNING: killing 13507 states (over memory cap)
KLEE: WARNING: killing 12258 states (over memory cap)
KLEE: WARNING: killing 12637 states (over memory cap)
KLEE: WARNING: killing 12673 states (over memory cap)
KLEE: WARNING: killing 12905 states (over memory cap)
KLEE: WARNING: killing 13233 states (over memory cap)
KLEE: WARNING: killing 12681 states (over memory cap)
KLEE: WARNING: killing 12723 states (over memory cap)
KLEE: WARNING: killing 13198 states (over memory cap)
KLEE: WARNING: killing 12304 states (over memory cap)
KLEE: WARNING: killing 13322 states (over memory cap)
KLEE: WARNING: killing 12871 states (over memory cap)
KLEE: WARNING: killing 13000 states (over memory cap)
KLEE: WARNING: killing 12795 states (over memory cap)
KLEE: WARNING: killing 13078 states (over memory cap)
KLEE: WARNING: killing 12573 states (over memory cap)
KLEE: WARNING: killing 12660 states (over memory cap)
KLEE: WARNING: killing 13131 states (over memory cap)
KLEE: WARNING: killing 12584 states (over memory cap)
KLEE: WARNING: killing 12430 states (over memory cap)
KLEE: WARNING: killing 12753 states (over memory cap)
KLEE: WARNING: killing 12844 states (over memory cap)
KLEE: WARNING: killing 12442 states (over memory cap)
KLEE: WARNING: killing 13355 states (over memory cap)
KLEE: WARNING: killing 12565 states (over memory cap)
KLEE: WARNING: killing 12700 states (over memory cap)
KLEE: WARNING: killing 12591 states (over memory cap)
KLEE: WARNING: killing 12528 states (over memory cap)
KLEE: WARNING: killing 13289 states (over memory cap)
KLEE: WARNING: killing 12844 states (over memory cap)
KLEE: WARNING: killing 12736 states (over memory cap)
KLEE: WARNING: killing 13210 states (over memory cap)
KLEE: WARNING: killing 12958 states (over memory cap)
KLEE: WARNING: killing 12613 states (over memory cap)
KLEE: WARNING: killing 13032 states (over memory cap)
KLEE: WARNING: killing 12491 states (over memory cap)
KLEE: WARNING: killing 12718 states (over memory cap)
KLEE: WARNING: killing 13092 states (over memory cap)
KLEE: WARNING: killing 13030 states (over memory cap)
KLEE: WARNING: killing 12685 states (over memory cap)
KLEE: WARNING: killing 12439 states (over memory cap)
KLEE: WARNING: killing 12904 states (over memory cap)
KLEE: WARNING: killing 12801 states (over memory cap)
KLEE: WARNING: killing 12790 states (over memory cap)
KLEE: WARNING: killing 12919 states (over memory cap)
KLEE: WARNING: killing 12387 states (over memory cap)
KLEE: WARNING: killing 13231 states (over memory cap)
KLEE: WARNING: killing 12270 states (over memory cap)
KLEE: WARNING: killing 12453 states (over memory cap)
KLEE: WARNING: killing 12435 states (over memory cap)
KLEE: WARNING: killing 12760 states (over memory cap)
KLEE: WARNING: killing 12462 states (over memory cap)
KLEE: WARNING: killing 13165 states (over memory cap)
KLEE: WARNING: killing 13296 states (over memory cap)
KLEE: WARNING: killing 12816 states (over memory cap)
KLEE: WARNING: killing 13093 states (over memory cap)
KLEE: WARNING: killing 12936 states (over memory cap)
KLEE: WARNING: killing 13113 states (over memory cap)
KLEE: WARNING: killing 12350 states (over memory cap)
KLEE: WARNING: killing 13098 states (over memory cap)
KLEE: WARNING: killing 12331 states (over memory cap)
KLEE: WARNING: killing 12607 states (over memory cap)
KLEE: WARNING: killing 12832 states (over memory cap)
KLEE: WARNING: killing 12960 states (over memory cap)
KLEE: WARNING: killing 12575 states (over memory cap)
KLEE: WARNING: killing 12325 states (over memory cap)
KLEE: WARNING: killing 13067 states (over memory cap)
KLEE: WARNING: killing 13152 states (over memory cap)
KLEE: WARNING: killing 12673 states (over memory cap)
KLEE: WARNING: killing 13314 states (over memory cap)
KLEE: WARNING: killing 12792 states (over memory cap)
KLEE: WARNING: killing 12551 states (over memory cap)
KLEE: WARNING: killing 12581 states (over memory cap)
KLEE: WARNING: killing 13455 states (over memory cap)
KLEE: WARNING: killing 12564 states (over memory cap)
KLEE: WARNING: killing 12505 states (over memory cap)
KLEE: WARNING: killing 12866 states (over memory cap)
KLEE: WARNING: killing 12766 states (over memory cap)
KLEE: WARNING: killing 12892 states (over memory cap)
KLEE: WARNING: killing 13345 states (over memory cap)
KLEE: WARNING: killing 12314 states (over memory cap)
KLEE: WARNING: killing 12812 states (over memory cap)
KLEE: WARNING: killing 12848 states (over memory cap)
KLEE: WARNING: killing 12516 states (over memory cap)
KLEE: WARNING: killing 12686 states (over memory cap)
KLEE: WARNING: killing 12675 states (over memory cap)
KLEE: WARNING: killing 13124 states (over memory cap)
KLEE: WARNING: killing 12750 states (over memory cap)
KLEE: WARNING: killing 12693 states (over memory cap)
KLEE: WARNING: killing 12909 states (over memory cap)
KLEE: WARNING: killing 12577 states (over memory cap)
KLEE: WARNING: killing 12935 states (over memory cap)
KLEE: WARNING: killing 13020 states (over memory cap)
KLEE: WARNING: killing 12411 states (over memory cap)
KLEE: WARNING: killing 12079 states (over memory cap)
KLEE: WARNING: killing 12842 states (over memory cap)
KLEE: WARNING: killing 12651 states (over memory cap)
KLEE: WARNING: killing 12550 states (over memory cap)
KLEE: WARNING: killing 13223 states (over memory cap)
KLEE: WARNING: killing 12843 states (over memory cap)
KLEE: WARNING: killing 12840 states (over memory cap)
KLEE: WARNING: killing 12828 states (over memory cap)
KLEE: WARNING: killing 12772 states (over memory cap)
KLEE: WARNING: killing 12757 states (over memory cap)
KLEE: WARNING: killing 12793 states (over memory cap)
KLEE: WARNING: killing 13510 states (over memory cap)
KLEE: WARNING: killing 12822 states (over memory cap)
KLEE: WARNING: killing 12226 states (over memory cap)
KLEE: WARNING: killing 12527 states (over memory cap)
KLEE: WARNING: killing 13151 states (over memory cap)
KLEE: WARNING: killing 12689 states (over memory cap)
KLEE: WARNING: killing 12852 states (over memory cap)
KLEE: WARNING: killing 12666 states (over memory cap)
KLEE: WARNING: killing 12433 states (over memory cap)
KLEE: WARNING: killing 13094 states (over memory cap)
KLEE: WARNING: killing 13132 states (over memory cap)
KLEE: WARNING: killing 13077 states (over memory cap)
KLEE: WARNING: killing 12298 states (over memory cap)
KLEE: WARNING: killing 12831 states (over memory cap)
KLEE: WARNING: killing 12953 states (over memory cap)
KLEE: WARNING: killing 12763 states (over memory cap)
KLEE: WARNING: killing 13066 states (over memory cap)
KLEE: WARNING: killing 12697 states (over memory cap)
KLEE: WARNING: killing 13229 states (over memory cap)
KLEE: WARNING: killing 12053 states (over memory cap)
KLEE: WARNING: killing 12490 states (over memory cap)
KLEE: WARNING: killing 12659 states (over memory cap)
KLEE: WARNING: killing 13324 states (over memory cap)
KLEE: WARNING: killing 12907 states (over memory cap)
KLEE: WARNING: killing 13169 states (over memory cap)
KLEE: WARNING: killing 12801 states (over memory cap)
KLEE: WARNING: killing 12919 states (over memory cap)
KLEE: WARNING: killing 12785 states (over memory cap)
KLEE: WARNING: killing 12815 states (over memory cap)
KLEE: WARNING: killing 12892 states (over memory cap)
KLEE: WARNING: killing 13199 states (over memory cap)
KLEE: WARNING: killing 12211 states (over memory cap)
KLEE: WARNING: killing 13086 states (over memory cap)
KLEE: WARNING: killing 13342 states (over memory cap)
KLEE: WARNING: killing 13242 states (over memory cap)
KLEE: WARNING: killing 13235 states (over memory cap)
KLEE: WARNING: killing 12257 states (over memory cap)
KLEE: WARNING: killing 12689 states (over memory cap)
KLEE: WARNING: killing 12637 states (over memory cap)
KLEE: WARNING: killing 12534 states (over memory cap)
KLEE: WARNING: killing 12830 states (over memory cap)
KLEE: WARNING: killing 12866 states (over memory cap)
KLEE: WARNING: killing 12677 states (over memory cap)
