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-kernel-locking-mutex__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.: 339 303 2584 16489
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.649851799011
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
Defining function rndis_command as symbolic
Defining function netdev_warn as symbolic
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
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
Defining function krealloc 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)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Defining function round_jiffies_relative as symbolic
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
Defining function external_allocated_data as symbolic
Removed calls to 'usbnet_tx_timeout' (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)
Removed calls to 'ldv_assert' (function is undefined)
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.575946092606
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 309 273 1037 8089
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_f01bc2cf-c4d9-49e5-ad11-aee88291b5c1/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 22119 states (over memory cap)
KLEE: WARNING: killing 12935 states (over memory cap)
KLEE: WARNING: killing 12065 states (over memory cap)
KLEE: WARNING: killing 12035 states (over memory cap)
KLEE: WARNING: killing 22471 states (over memory cap)
KLEE: WARNING: killing 12561 states (over memory cap)
KLEE: WARNING: killing 22713 states (over memory cap)
KLEE: WARNING: killing 22756 states (over memory cap)
KLEE: WARNING: killing 12344 states (over memory cap)
KLEE: WARNING: killing 23015 states (over memory cap)
KLEE: WARNING: killing 12286 states (over memory cap)
KLEE: WARNING: killing 12386 states (over memory cap)
KLEE: WARNING: killing 12835 states (over memory cap)
KLEE: WARNING: killing 12114 states (over memory cap)
KLEE: WARNING: killing 12332 states (over memory cap)
KLEE: WARNING: killing 12424 states (over memory cap)
KLEE: WARNING: killing 12639 states (over memory cap)
KLEE: WARNING: killing 13202 states (over memory cap)
KLEE: WARNING: killing 12714 states (over memory cap)
KLEE: WARNING: killing 12813 states (over memory cap)
KLEE: WARNING: killing 13260 states (over memory cap)
KLEE: WARNING: killing 13473 states (over memory cap)
KLEE: WARNING: killing 13227 states (over memory cap)
KLEE: WARNING: killing 14019 states (over memory cap)
KLEE: WARNING: killing 13187 states (over memory cap)
KLEE: WARNING: killing 13516 states (over memory cap)
KLEE: WARNING: killing 13268 states (over memory cap)
KLEE: WARNING: killing 13824 states (over memory cap)
KLEE: WARNING: killing 13353 states (over memory cap)
KLEE: WARNING: killing 12992 states (over memory cap)
KLEE: WARNING: killing 13093 states (over memory cap)
KLEE: WARNING: killing 13644 states (over memory cap)
KLEE: WARNING: killing 12942 states (over memory cap)
KLEE: WARNING: killing 13270 states (over memory cap)
KLEE: WARNING: killing 13031 states (over memory cap)
KLEE: WARNING: killing 13131 states (over memory cap)
KLEE: WARNING: killing 12892 states (over memory cap)
KLEE: WARNING: killing 12990 states (over memory cap)
KLEE: WARNING: killing 13086 states (over memory cap)
KLEE: WARNING: killing 12504 states (over memory cap)
KLEE: WARNING: killing 12150 states (over memory cap)
KLEE: WARNING: killing 12809 states (over memory cap)
KLEE: WARNING: killing 12576 states (over memory cap)
KLEE: WARNING: killing 12668 states (over memory cap)
KLEE: WARNING: killing 11864 states (over memory cap)
KLEE: WARNING: killing 12301 states (over memory cap)
KLEE: WARNING: killing 12058 states (over memory cap)
KLEE: WARNING: killing 12157 states (over memory cap)
KLEE: WARNING: killing 12933 states (over memory cap)
KLEE: WARNING: killing 12359 states (over memory cap)
KLEE: WARNING: killing 13465 states (over memory cap)
KLEE: WARNING: killing 12450 states (over memory cap)
KLEE: WARNING: killing 13108 states (over memory cap)
KLEE: WARNING: killing 12645 states (over memory cap)
KLEE: WARNING: killing 12409 states (over memory cap)
KLEE: WARNING: killing 12616 states (over memory cap)
KLEE: WARNING: killing 12605 states (over memory cap)
KLEE: WARNING: killing 12583 states (over memory cap)
KLEE: WARNING: killing 12793 states (over memory cap)
KLEE: WARNING: killing 12778 states (over memory cap)
KLEE: WARNING: killing 12432 states (over memory cap)
KLEE: WARNING: killing 13194 states (over memory cap)
KLEE: WARNING: killing 12628 states (over memory cap)
KLEE: WARNING: killing 12727 states (over memory cap)
KLEE: WARNING: killing 13267 states (over memory cap)
KLEE: WARNING: killing 12373 states (over memory cap)
KLEE: WARNING: killing 12913 states (over memory cap)
KLEE: WARNING: killing 13011 states (over memory cap)
KLEE: WARNING: killing 12449 states (over memory cap)
KLEE: WARNING: killing 12874 states (over memory cap)
KLEE: WARNING: killing 13193 states (over memory cap)
KLEE: WARNING: killing 13068 states (over memory cap)
KLEE: WARNING: killing 12503 states (over memory cap)
KLEE: WARNING: killing 12712 states (over memory cap)
KLEE: WARNING: killing 12921 states (over memory cap)
KLEE: WARNING: killing 13346 states (over memory cap)
KLEE: WARNING: killing 12572 states (over memory cap)
KLEE: WARNING: killing 12557 states (over memory cap)
KLEE: WARNING: killing 12322 states (over memory cap)
KLEE: WARNING: killing 12633 states (over memory cap)
KLEE: WARNING: killing 12515 states (over memory cap)
KLEE: WARNING: killing 12281 states (over memory cap)
KLEE: WARNING: killing 12592 states (over memory cap)
KLEE: WARNING: killing 12473 states (over memory cap)
KLEE: WARNING: killing 12459 states (over memory cap)
KLEE: WARNING: killing 13310 states (over memory cap)
KLEE: WARNING: killing 12328 states (over memory cap)
KLEE: WARNING: killing 12203 states (over memory cap)
KLEE: WARNING: killing 12947 states (over memory cap)
KLEE: WARNING: killing 12510 states (over memory cap)
KLEE: WARNING: killing 12929 states (over memory cap)
KLEE: WARNING: killing 12374 states (over memory cap)
KLEE: WARNING: killing 12794 states (over memory cap)
KLEE: WARNING: killing 12894 states (over memory cap)
KLEE: WARNING: killing 12345 states (over memory cap)
KLEE: WARNING: killing 13080 states (over memory cap)
KLEE: WARNING: killing 11895 states (over memory cap)
KLEE: WARNING: killing 12304 states (over memory cap)
KLEE: WARNING: killing 13259 states (over memory cap)
KLEE: WARNING: killing 12600 states (over memory cap)
KLEE: WARNING: killing 12805 states (over memory cap)
KLEE: WARNING: killing 12048 states (over memory cap)
KLEE: WARNING: killing 13206 states (over memory cap)
KLEE: WARNING: killing 12557 states (over memory cap)
KLEE: WARNING: killing 12541 states (over memory cap)
KLEE: WARNING: killing 12638 states (over memory cap)
KLEE: WARNING: killing 12843 states (over memory cap)
KLEE: WARNING: killing 12616 states (over memory cap)
KLEE: WARNING: killing 12713 states (over memory cap)
KLEE: WARNING: killing 12592 states (over memory cap)
KLEE: WARNING: killing 12582 states (over memory cap)
KLEE: WARNING: killing 13416 states (over memory cap)
KLEE: WARNING: killing 12456 states (over memory cap)
KLEE: WARNING: killing 12973 states (over memory cap)
KLEE: WARNING: killing 12852 states (over memory cap)
KLEE: WARNING: killing 12736 states (over memory cap)
KLEE: WARNING: killing 12726 states (over memory cap)
KLEE: WARNING: killing 12715 states (over memory cap)
KLEE: WARNING: killing 12702 states (over memory cap)
KLEE: WARNING: killing 12274 states (over memory cap)
KLEE: WARNING: killing 12681 states (over memory cap)
KLEE: WARNING: killing 12668 states (over memory cap)
KLEE: WARNING: killing 12344 states (over memory cap)
KLEE: WARNING: killing 12536 states (over memory cap)
KLEE: WARNING: killing 12524 states (over memory cap)
KLEE: WARNING: killing 12618 states (over memory cap)
KLEE: WARNING: killing 12607 states (over memory cap)
KLEE: WARNING: killing 13223 states (over memory cap)
KLEE: WARNING: killing 12381 states (over memory cap)
KLEE: WARNING: killing 12891 states (over memory cap)
KLEE: WARNING: killing 11940 states (over memory cap)
KLEE: WARNING: killing 12134 states (over memory cap)
KLEE: WARNING: killing 12744 states (over memory cap)
KLEE: WARNING: killing 12736 states (over memory cap)
KLEE: WARNING: killing 12420 states (over memory cap)
KLEE: WARNING: killing 12926 states (over memory cap)
KLEE: WARNING: killing 12710 states (over memory cap)
KLEE: WARNING: killing 12799 states (over memory cap)
KLEE: WARNING: killing 12370 states (over memory cap)
KLEE: WARNING: killing 12465 states (over memory cap)
KLEE: WARNING: killing 12346 states (over memory cap)
KLEE: WARNING: killing 12850 states (over memory cap)
KLEE: WARNING: killing 12633 states (over memory cap)
KLEE: WARNING: killing 12626 states (over memory cap)
KLEE: WARNING: killing 12615 states (over memory cap)
KLEE: WARNING: killing 12602 states (over memory cap)
KLEE: WARNING: killing 12690 states (over memory cap)
KLEE: WARNING: killing 12781 states (over memory cap)
KLEE: WARNING: killing 13180 states (over memory cap)
KLEE: WARNING: killing 12971 states (over memory cap)
KLEE: WARNING: killing 12544 states (over memory cap)
KLEE: WARNING: killing 12231 states (over memory cap)
KLEE: WARNING: killing 13039 states (over memory cap)
KLEE: WARNING: killing 13132 states (over memory cap)
KLEE: WARNING: killing 12817 states (over memory cap)
KLEE: WARNING: killing 12908 states (over memory cap)
KLEE: WARNING: killing 12686 states (over memory cap)
KLEE: WARNING: killing 12576 states (over memory cap)
KLEE: WARNING: killing 12767 states (over memory cap)
KLEE: WARNING: killing 12349 states (over memory cap)
KLEE: WARNING: killing 11931 states (over memory cap)
KLEE: WARNING: killing 12531 states (over memory cap)
KLEE: WARNING: killing 13022 states (over memory cap)
KLEE: WARNING: killing 12910 states (over memory cap)
KLEE: WARNING: killing 12903 states (over memory cap)
KLEE: WARNING: killing 12287 states (over memory cap)
KLEE: WARNING: killing 12784 states (over memory cap)
KLEE: WARNING: killing 13071 states (over memory cap)
KLEE: WARNING: killing 12757 states (over memory cap)
KLEE: WARNING: killing 12747 states (over memory cap)
KLEE: WARNING: killing 12834 states (over memory cap)
KLEE: WARNING: killing 12224 states (over memory cap)
KLEE: WARNING: killing 12211 states (over memory cap)
KLEE: WARNING: killing 13096 states (over memory cap)
KLEE: WARNING: killing 11791 states (over memory cap)
KLEE: WARNING: killing 12580 states (over memory cap)
KLEE: WARNING: killing 12665 states (over memory cap)
KLEE: WARNING: killing 12259 states (over memory cap)
KLEE: WARNING: killing 12747 states (over memory cap)
KLEE: WARNING: killing 12637 states (over memory cap)
KLEE: WARNING: killing 12522 states (over memory cap)
KLEE: WARNING: killing 12714 states (over memory cap)
KLEE: WARNING: killing 12600 states (over memory cap)
KLEE: WARNING: killing 12396 states (over memory cap)
KLEE: WARNING: killing 12679 states (over memory cap)
KLEE: WARNING: killing 12669 states (over memory cap)
KLEE: WARNING: killing 12456 states (over memory cap)
KLEE: WARNING: killing 12645 states (over memory cap)
KLEE: WARNING: killing 12441 states (over memory cap)
KLEE: WARNING: killing 12226 states (over memory cap)
KLEE: WARNING: killing 12419 states (over memory cap)
KLEE: WARNING: killing 12206 states (over memory cap)
KLEE: WARNING: killing 12795 states (over memory cap)
KLEE: WARNING: killing 12684 states (over memory cap)
KLEE: WARNING: killing 11985 states (over memory cap)
KLEE: WARNING: killing 13053 states (over memory cap)
KLEE: WARNING: killing 12552 states (over memory cap)
KLEE: WARNING: killing 12244 states (over memory cap)
KLEE: WARNING: killing 13023 states (over memory cap)
KLEE: WARNING: killing 13401 states (over memory cap)
KLEE: WARNING: killing 13094 states (over memory cap)
KLEE: WARNING: killing 12989 states (over memory cap)
KLEE: WARNING: killing 12294 states (over memory cap)
KLEE: WARNING: killing 12767 states (over memory cap)
KLEE: WARNING: killing 12269 states (over memory cap)
KLEE: WARNING: killing 12358 states (over memory cap)
KLEE: WARNING: killing 12053 states (over memory cap)
KLEE: WARNING: killing 12335 states (over memory cap)
KLEE: WARNING: killing 12907 states (over memory cap)
KLEE: WARNING: killing 12608 states (over memory cap)
KLEE: WARNING: killing 12497 states (over memory cap)
KLEE: WARNING: killing 12488 states (over memory cap)
KLEE: WARNING: killing 12382 states (over memory cap)
KLEE: WARNING: killing 13437 states (over memory cap)
KLEE: WARNING: killing 12941 states (over memory cap)
KLEE: WARNING: killing 12737 states (over memory cap)
KLEE: WARNING: killing 12150 states (over memory cap)
KLEE: WARNING: killing 12523 states (over memory cap)
KLEE: WARNING: killing 12700 states (over memory cap)
KLEE: WARNING: killing 12877 states (over memory cap)
KLEE: WARNING: killing 12771 states (over memory cap)
KLEE: WARNING: killing 12474 states (over memory cap)
KLEE: WARNING: killing 12467 states (over memory cap)
