bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-challenges/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-wireless-rndis_wlan_true-unreach-call.cil.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.: 350 365 2771 17386
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.666344881058
Defining function usbnet_open as symbolic
Defining function eth_mac_addr as symbolic
Defining function queue_work_on as symbolic
Defining function usbnet_start_xmit as symbolic
Defining function usbnet_stop as symbolic
Defining function eth_validate_addr as symbolic
Removed calls to 'usb_deregister' (function is undefined)
Defining function usb_register_driver as symbolic
Defining function ldv_pre_usb_register_driver as symbolic
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function rndis_command as symbolic
Defining function external_allocated_data as symbolic
Defining function netdev_warn as symbolic
Removed calls to 'usbnet_purge_paused_rxq' (function is undefined)
Removed calls to 'usbnet_resume_rx' (function is undefined)
Defining function ieee80211_frequency_to_channel as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
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
Removed calls to 'usbnet_pause_rx' (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
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Defining function round_jiffies_relative as symbolic
Removed calls to 'ldv_assert' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Defining function rndis_rx_fixup as symbolic
Defining function rndis_tx_fixup as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'rndis_unbind' (function is undefined)
Removed calls to 'wiphy_unregister' (function is undefined)
Removed calls to 'wiphy_free' (function is undefined)
Defining function cancel_delayed_work_sync as symbolic
Defining function cancel_work_sync as symbolic
Defining function sprintf 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 'cfg80211_scan_done' (function is undefined)
Defining function wiphy_new as symbolic
Defining function __alloc_workqueue_key as symbolic
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 netdev_err as symbolic
Removed calls to 'usbnet_tx_timeout' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'rndis_status' (function is undefined)
Removed calls to 'ldv_switch_to_interrupt_context' (function is undefined)
Removed calls to 'ldv_switch_to_process_context' (function is undefined)
Removed calls to 'usbnet_disconnect' (function is undefined)
Removed calls to 'ldv_pre_probe' (function is undefined)
Linked our definitions to these undefined functions:
  strcmp
  strcpy
  strlen
  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.587464094162
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 316 337 1078 8678
INFO: Starting verification
KLEE: WARNING ONCE: function "rndis_wlan_set_multicast_list" has inline asm
KLEE: WARNING ONCE: function "rndis_add_key" has inline asm
KLEE: WARNING ONCE: function "rndis_change_virtual_intf" has inline asm
KLEE: WARNING ONCE: function "rndis_del_key" has inline asm
KLEE: WARNING ONCE: function "rndis_del_pmksa" has inline asm
KLEE: WARNING ONCE: function "rndis_dump_station" has inline asm
KLEE: WARNING ONCE: function "rndis_flush_pmksa" has inline asm
KLEE: WARNING ONCE: function "rndis_get_station" 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_set_cqm_rssi_config" has inline asm
KLEE: WARNING ONCE: function "rndis_set_default_key" has inline asm
KLEE: WARNING ONCE: function "rndis_set_pmksa" has inline asm
KLEE: WARNING ONCE: function "rndis_set_power_mgmt" has inline asm
KLEE: WARNING ONCE: function "rndis_set_tx_power" has inline asm
KLEE: WARNING ONCE: function "rndis_set_wiphy_params" has inline asm
KLEE: WARNING ONCE: function "rndis_wlan_indication" 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 "ldv_struct_cfg80211_ops_io_instance_1" has inline asm
KLEE: WARNING ONCE: function "ldv_io_instance_callback_1_28" has inline asm
KLEE: WARNING ONCE: function "ldv_io_instance_callback_1_35" has inline asm
KLEE: WARNING ONCE: function "ldv_io_instance_callback_1_41" 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: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_19689e75-d9eb-4b1a-abe3-67cee3650ce8/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 18925 states (over memory cap)
KLEE: WARNING: killing 12939 states (over memory cap)
KLEE: WARNING: killing 22780 states (over memory cap)
KLEE: WARNING: killing 22919 states (over memory cap)
KLEE: WARNING: killing 23684 states (over memory cap)
KLEE: WARNING: killing 12521 states (over memory cap)
KLEE: WARNING: killing 12021 states (over memory cap)
KLEE: WARNING: killing 22704 states (over memory cap)
KLEE: WARNING: killing 12204 states (over memory cap)
KLEE: WARNING: killing 22845 states (over memory cap)
KLEE: WARNING: killing 12386 states (over memory cap)
KLEE: WARNING: killing 12011 states (over memory cap)
KLEE: WARNING: killing 12109 states (over memory cap)
KLEE: WARNING: killing 12559 states (over memory cap)
KLEE: WARNING: killing 12424 states (over memory cap)
KLEE: WARNING: killing 12643 states (over memory cap)
KLEE: WARNING: killing 12507 states (over memory cap)
KLEE: WARNING: killing 12951 states (over memory cap)
KLEE: WARNING: killing 12932 states (over memory cap)
KLEE: WARNING: killing 13262 states (over memory cap)
KLEE: WARNING: killing 12897 states (over memory cap)
KLEE: WARNING: killing 13925 states (over memory cap)
KLEE: WARNING: killing 14264 states (over memory cap)
KLEE: WARNING: killing 13886 states (over memory cap)
KLEE: WARNING: killing 12938 states (over memory cap)
KLEE: WARNING: killing 13851 states (over memory cap)
KLEE: WARNING: killing 13258 states (over memory cap)
KLEE: WARNING: killing 13353 states (over memory cap)
KLEE: WARNING: killing 13687 states (over memory cap)
KLEE: WARNING: killing 13206 states (over memory cap)
KLEE: WARNING: killing 13537 states (over memory cap)
KLEE: WARNING: killing 13061 states (over memory cap)
KLEE: WARNING: killing 13276 states (over memory cap)
KLEE: WARNING: killing 13607 states (over memory cap)
KLEE: WARNING: killing 12790 states (over memory cap)
KLEE: WARNING: killing 13465 states (over memory cap)
KLEE: WARNING: killing 13216 states (over memory cap)
KLEE: WARNING: killing 12402 states (over memory cap)
KLEE: WARNING: killing 12387 states (over memory cap)
KLEE: WARNING: killing 12489 states (over memory cap)
KLEE: WARNING: killing 13155 states (over memory cap)
KLEE: WARNING: killing 13030 states (over memory cap)
KLEE: WARNING: killing 12444 states (over memory cap)
KLEE: WARNING: killing 12994 states (over memory cap)
KLEE: WARNING: killing 12752 states (over memory cap)
KLEE: WARNING: killing 12737 states (over memory cap)
KLEE: WARNING: killing 12379 states (over memory cap)
KLEE: WARNING: killing 12141 states (over memory cap)
KLEE: WARNING: killing 12695 states (over memory cap)
KLEE: WARNING: killing 13018 states (over memory cap)
KLEE: WARNING: killing 11878 states (over memory cap)
KLEE: WARNING: killing 12309 states (over memory cap)
KLEE: WARNING: killing 12750 states (over memory cap)
KLEE: WARNING: killing 12398 states (over memory cap)
KLEE: WARNING: killing 12943 states (over memory cap)
KLEE: WARNING: killing 13380 states (over memory cap)
KLEE: WARNING: killing 13366 states (over memory cap)
KLEE: WARNING: killing 13019 states (over memory cap)
KLEE: WARNING: killing 13001 states (over memory cap)
KLEE: WARNING: killing 12429 states (over memory cap)
KLEE: WARNING: killing 12862 states (over memory cap)
KLEE: WARNING: killing 12515 states (over memory cap)
KLEE: WARNING: killing 12609 states (over memory cap)
KLEE: WARNING: killing 12376 states (over memory cap)
KLEE: WARNING: killing 12918 states (over memory cap)
KLEE: WARNING: killing 13013 states (over memory cap)
KLEE: WARNING: killing 12561 states (over memory cap)
KLEE: WARNING: killing 12879 states (over memory cap)
KLEE: WARNING: killing 13193 states (over memory cap)
KLEE: WARNING: killing 12301 states (over memory cap)
KLEE: WARNING: killing 13059 states (over memory cap)
KLEE: WARNING: killing 12608 states (over memory cap)
KLEE: WARNING: killing 13362 states (over memory cap)
KLEE: WARNING: killing 12358 states (over memory cap)
KLEE: WARNING: killing 12565 states (over memory cap)
KLEE: WARNING: killing 12551 states (over memory cap)
KLEE: WARNING: killing 12536 states (over memory cap)
KLEE: WARNING: killing 12310 states (over memory cap)
KLEE: WARNING: killing 12847 states (over memory cap)
KLEE: WARNING: killing 12945 states (over memory cap)
KLEE: WARNING: killing 12717 states (over memory cap)
KLEE: WARNING: killing 12592 states (over memory cap)
KLEE: WARNING: killing 13344 states (over memory cap)
KLEE: WARNING: killing 12134 states (over memory cap)
KLEE: WARNING: killing 12443 states (over memory cap)
KLEE: WARNING: killing 13305 states (over memory cap)
KLEE: WARNING: killing 12640 states (over memory cap)
KLEE: WARNING: killing 12624 states (over memory cap)
KLEE: WARNING: killing 13047 states (over memory cap)
KLEE: WARNING: killing 13146 states (over memory cap)
KLEE: WARNING: killing 12585 states (over memory cap)
KLEE: WARNING: killing 12576 states (over memory cap)
KLEE: WARNING: killing 12558 states (over memory cap)
KLEE: WARNING: killing 12553 states (over memory cap)
KLEE: WARNING: killing 12975 states (over memory cap)
KLEE: WARNING: killing 12849 states (over memory cap)
KLEE: WARNING: killing 12951 states (over memory cap)
KLEE: WARNING: killing 12506 states (over memory cap)
KLEE: WARNING: killing 12600 states (over memory cap)
KLEE: WARNING: killing 12912 states (over memory cap)
KLEE: WARNING: killing 12469 states (over memory cap)
KLEE: WARNING: killing 12667 states (over memory cap)
KLEE: WARNING: killing 13090 states (over memory cap)
KLEE: WARNING: killing 12869 states (over memory cap)
KLEE: WARNING: killing 12639 states (over memory cap)
KLEE: WARNING: killing 12304 states (over memory cap)
KLEE: WARNING: killing 12508 states (over memory cap)
KLEE: WARNING: killing 12495 states (over memory cap)
KLEE: WARNING: killing 13017 states (over memory cap)
KLEE: WARNING: killing 13005 states (over memory cap)
KLEE: WARNING: killing 12671 states (over memory cap)
KLEE: WARNING: killing 12762 states (over memory cap)
KLEE: WARNING: killing 13283 states (over memory cap)
KLEE: WARNING: killing 12319 states (over memory cap)
KLEE: WARNING: killing 12515 states (over memory cap)
KLEE: WARNING: killing 12396 states (over memory cap)
KLEE: WARNING: killing 12704 states (over memory cap)
KLEE: WARNING: killing 13328 states (over memory cap)
KLEE: WARNING: killing 12369 states (over memory cap)
KLEE: WARNING: killing 12145 states (over memory cap)
KLEE: WARNING: killing 12763 states (over memory cap)
KLEE: WARNING: killing 13067 states (over memory cap)
KLEE: WARNING: killing 12530 states (over memory cap)
KLEE: WARNING: killing 12519 states (over memory cap)
KLEE: WARNING: killing 12611 states (over memory cap)
KLEE: WARNING: killing 12812 states (over memory cap)
KLEE: WARNING: killing 13010 states (over memory cap)
KLEE: WARNING: killing 12787 states (over memory cap)
KLEE: WARNING: killing 13090 states (over memory cap)
KLEE: WARNING: killing 12244 states (over memory cap)
KLEE: WARNING: killing 13274 states (over memory cap)
KLEE: WARNING: killing 13052 states (over memory cap)
KLEE: WARNING: killing 12519 states (over memory cap)
KLEE: WARNING: killing 12923 states (over memory cap)
KLEE: WARNING: killing 13540 states (over memory cap)
KLEE: WARNING: killing 12902 states (over memory cap)
KLEE: WARNING: killing 12478 states (over memory cap)
KLEE: WARNING: killing 12882 states (over memory cap)
KLEE: WARNING: killing 11936 states (over memory cap)
KLEE: WARNING: killing 11818 states (over memory cap)
KLEE: WARNING: killing 13465 states (over memory cap)
KLEE: WARNING: killing 12314 states (over memory cap)
KLEE: WARNING: killing 12204 states (over memory cap)
KLEE: WARNING: killing 12599 states (over memory cap)
KLEE: WARNING: killing 12178 states (over memory cap)
KLEE: WARNING: killing 12782 states (over memory cap)
KLEE: WARNING: killing 13291 states (over memory cap)
KLEE: WARNING: killing 12254 states (over memory cap)
KLEE: WARNING: killing 12857 states (over memory cap)
KLEE: WARNING: killing 12845 states (over memory cap)
KLEE: WARNING: killing 12730 states (over memory cap)
KLEE: WARNING: killing 12623 states (over memory cap)
KLEE: WARNING: killing 12406 states (over memory cap)
KLEE: WARNING: killing 12292 states (over memory cap)
KLEE: WARNING: killing 12484 states (over memory cap)
KLEE: WARNING: killing 12990 states (over memory cap)
KLEE: WARNING: killing 12567 states (over memory cap)
KLEE: WARNING: killing 12963 states (over memory cap)
KLEE: WARNING: killing 12751 states (over memory cap)
KLEE: WARNING: killing 12125 states (over memory cap)
KLEE: WARNING: killing 12820 states (over memory cap)
KLEE: WARNING: killing 12815 states (over memory cap)
KLEE: WARNING: killing 13214 states (over memory cap)
KLEE: WARNING: killing 12898 states (over memory cap)
KLEE: WARNING: killing 12783 states (over memory cap)
KLEE: WARNING: killing 12668 states (over memory cap)
KLEE: WARNING: killing 12860 states (over memory cap)
KLEE: WARNING: killing 12952 states (over memory cap)
KLEE: WARNING: killing 12939 states (over memory cap)
KLEE: WARNING: killing 12621 states (over memory cap)
KLEE: WARNING: killing 12609 states (over memory cap)
KLEE: WARNING: killing 12499 states (over memory cap)
KLEE: WARNING: killing 12893 states (over memory cap)
KLEE: WARNING: killing 12583 states (over memory cap)
KLEE: WARNING: killing 12473 states (over memory cap)
KLEE: WARNING: killing 12364 states (over memory cap)
KLEE: WARNING: killing 12354 states (over memory cap)
KLEE: WARNING: killing 12941 states (over memory cap)
KLEE: WARNING: killing 12533 states (over memory cap)
KLEE: WARNING: killing 12521 states (over memory cap)
KLEE: WARNING: killing 12915 states (over memory cap)
KLEE: WARNING: killing 12803 states (over memory cap)
KLEE: WARNING: killing 12890 states (over memory cap)
KLEE: WARNING: killing 12480 states (over memory cap)
KLEE: WARNING: killing 12868 states (over memory cap)
KLEE: WARNING: killing 12952 states (over memory cap)
KLEE: WARNING: killing 12644 states (over memory cap)
KLEE: WARNING: killing 12826 states (over memory cap)
KLEE: WARNING: killing 12022 states (over memory cap)
KLEE: WARNING: killing 12509 states (over memory cap)
KLEE: WARNING: killing 12205 states (over memory cap)
KLEE: WARNING: killing 12791 states (over memory cap)
KLEE: WARNING: killing 12678 states (over memory cap)
KLEE: WARNING: killing 12570 states (over memory cap)
KLEE: WARNING: killing 12557 states (over memory cap)
KLEE: WARNING: killing 12150 states (over memory cap)
KLEE: WARNING: killing 12832 states (over memory cap)
KLEE: WARNING: killing 12922 states (over memory cap)
KLEE: WARNING: killing 12711 states (over memory cap)
KLEE: WARNING: killing 12504 states (over memory cap)
KLEE: WARNING: killing 12789 states (over memory cap)
KLEE: WARNING: killing 12782 states (over memory cap)
KLEE: WARNING: killing 12082 states (over memory cap)
KLEE: WARNING: killing 12662 states (over memory cap)
KLEE: WARNING: killing 13340 states (over memory cap)
KLEE: WARNING: killing 12247 states (over memory cap)
KLEE: WARNING: killing 12623 states (over memory cap)
KLEE: WARNING: killing 12418 states (over memory cap)
KLEE: WARNING: killing 12896 states (over memory cap)
KLEE: WARNING: killing 12978 states (over memory cap)
KLEE: WARNING: killing 12578 states (over memory cap)
KLEE: WARNING: killing 12763 states (over memory cap)
KLEE: WARNING: killing 12562 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-mQqgxF/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-wireless-rndis_wlan_true-unreach-call.cil.c:6758: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12944 states (over memory cap)
KLEE: WARNING: killing 12643 states (over memory cap)
KLEE: WARNING: killing 13017 states (over memory cap)
KLEE: WARNING: killing 12321 states (over memory cap)
KLEE: WARNING: killing 12405 states (over memory cap)
KLEE: WARNING: killing 12687 states (over memory cap)
KLEE: WARNING: killing 12191 states (over memory cap)
KLEE: WARNING: killing 12373 states (over memory cap)
KLEE: WARNING: killing 13141 states (over memory cap)
KLEE: WARNING: killing 12841 states (over memory cap)
