bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.14/linux-3.14__complex_emg__linux-usb-dev__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.: 336 287 2539 16223
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.645101070404
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 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
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.554044961929
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 306 262 956 7820
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_84a0fdfc-e378-49cd-9911-fa3f8619f15d/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 20836 states (over memory cap)
KLEE: WARNING: killing 12548 states (over memory cap)
KLEE: WARNING: killing 23596 states (over memory cap)
KLEE: WARNING: killing 12108 states (over memory cap)
KLEE: WARNING: killing 23221 states (over memory cap)
KLEE: WARNING: killing 22417 states (over memory cap)
KLEE: WARNING: killing 12123 states (over memory cap)
KLEE: WARNING: killing 22670 states (over memory cap)
KLEE: WARNING: killing 12069 states (over memory cap)
KLEE: WARNING: killing 22563 states (over memory cap)
KLEE: WARNING: killing 12603 states (over memory cap)
KLEE: WARNING: killing 12345 states (over memory cap)
KLEE: WARNING: killing 11966 states (over memory cap)
KLEE: WARNING: killing 12072 states (over memory cap)
KLEE: WARNING: killing 12405 states (over memory cap)
KLEE: WARNING: killing 13324 states (over memory cap)
KLEE: WARNING: killing 12481 states (over memory cap)
KLEE: WARNING: killing 13051 states (over memory cap)
KLEE: WARNING: killing 13267 states (over memory cap)
KLEE: WARNING: killing 13718 states (over memory cap)
KLEE: WARNING: killing 13457 states (over memory cap)
KLEE: WARNING: killing 13552 states (over memory cap)
KLEE: WARNING: killing 13072 states (over memory cap)
KLEE: WARNING: killing 13863 states (over memory cap)
KLEE: WARNING: killing 13850 states (over memory cap)
KLEE: WARNING: killing 13948 states (over memory cap)
KLEE: WARNING: killing 13239 states (over memory cap)
KLEE: WARNING: killing 13451 states (over memory cap)
KLEE: WARNING: killing 13090 states (over memory cap)
KLEE: WARNING: killing 14105 states (over memory cap)
KLEE: WARNING: killing 13404 states (over memory cap)
KLEE: WARNING: killing 13500 states (over memory cap)
KLEE: WARNING: killing 13025 states (over memory cap)
KLEE: WARNING: killing 13696 states (over memory cap)
KLEE: WARNING: killing 13567 states (over memory cap)
KLEE: WARNING: killing 13211 states (over memory cap)
KLEE: WARNING: killing 13307 states (over memory cap)
KLEE: WARNING: killing 12374 states (over memory cap)
KLEE: WARNING: killing 12247 states (over memory cap)
KLEE: WARNING: killing 12798 states (over memory cap)
KLEE: WARNING: killing 12554 states (over memory cap)
KLEE: WARNING: killing 12880 states (over memory cap)
KLEE: WARNING: killing 13095 states (over memory cap)
KLEE: WARNING: killing 12854 states (over memory cap)
KLEE: WARNING: killing 12953 states (over memory cap)
KLEE: WARNING: killing 12266 states (over memory cap)
KLEE: WARNING: killing 12585 states (over memory cap)
KLEE: WARNING: killing 12460 states (over memory cap)
KLEE: WARNING: killing 12111 states (over memory cap)
KLEE: WARNING: killing 12544 states (over memory cap)
KLEE: WARNING: killing 12189 states (over memory cap)
KLEE: WARNING: killing 12511 states (over memory cap)
KLEE: WARNING: killing 12390 states (over memory cap)
KLEE: WARNING: killing 12260 states (over memory cap)
KLEE: WARNING: killing 12808 states (over memory cap)
KLEE: WARNING: killing 13128 states (over memory cap)
KLEE: WARNING: killing 12672 states (over memory cap)
KLEE: WARNING: killing 12769 states (over memory cap)
KLEE: WARNING: killing 12309 states (over memory cap)
KLEE: WARNING: killing 13188 states (over memory cap)
KLEE: WARNING: killing 12946 states (over memory cap)
KLEE: WARNING: killing 12821 states (over memory cap)
KLEE: WARNING: killing 12694 states (over memory cap)
KLEE: WARNING: killing 12790 states (over memory cap)
KLEE: WARNING: killing 12669 states (over memory cap)
KLEE: WARNING: killing 12767 states (over memory cap)
KLEE: WARNING: killing 12753 states (over memory cap)
KLEE: WARNING: killing 12522 states (over memory cap)
KLEE: WARNING: killing 12509 states (over memory cap)
KLEE: WARNING: killing 13601 states (over memory cap)
KLEE: WARNING: killing 13148 states (over memory cap)
KLEE: WARNING: killing 12911 states (over memory cap)
KLEE: WARNING: killing 13008 states (over memory cap)
KLEE: WARNING: killing 12889 states (over memory cap)
KLEE: WARNING: killing 12768 states (over memory cap)
KLEE: WARNING: killing 12201 states (over memory cap)
KLEE: WARNING: killing 13066 states (over memory cap)
KLEE: WARNING: killing 12503 states (over memory cap)
KLEE: WARNING: killing 13153 states (over memory cap)
KLEE: WARNING: killing 12705 states (over memory cap)
KLEE: WARNING: killing 12471 states (over memory cap)
KLEE: WARNING: killing 12891 states (over memory cap)
KLEE: WARNING: killing 12880 states (over memory cap)
KLEE: WARNING: killing 12326 states (over memory cap)
KLEE: WARNING: killing 12418 states (over memory cap)
KLEE: WARNING: killing 12514 states (over memory cap)
KLEE: WARNING: killing 12827 states (over memory cap)
KLEE: WARNING: killing 12922 states (over memory cap)
KLEE: WARNING: killing 12912 states (over memory cap)
KLEE: WARNING: killing 13119 states (over memory cap)
KLEE: WARNING: killing 13106 states (over memory cap)
KLEE: WARNING: killing 12661 states (over memory cap)
KLEE: WARNING: killing 12216 states (over memory cap)
KLEE: WARNING: killing 12847 states (over memory cap)
KLEE: WARNING: killing 12836 states (over memory cap)
KLEE: WARNING: killing 12717 states (over memory cap)
KLEE: WARNING: killing 12809 states (over memory cap)
KLEE: WARNING: killing 13338 states (over memory cap)
KLEE: WARNING: killing 12790 states (over memory cap)
KLEE: WARNING: killing 12665 states (over memory cap)
KLEE: WARNING: killing 12650 states (over memory cap)
KLEE: WARNING: killing 12963 states (over memory cap)
KLEE: WARNING: killing 12739 states (over memory cap)
KLEE: WARNING: killing 12406 states (over memory cap)
KLEE: WARNING: killing 12496 states (over memory cap)
KLEE: WARNING: killing 12808 states (over memory cap)
KLEE: WARNING: killing 12685 states (over memory cap)
KLEE: WARNING: killing 12463 states (over memory cap)
KLEE: WARNING: killing 12455 states (over memory cap)
KLEE: WARNING: killing 13081 states (over memory cap)
KLEE: WARNING: killing 12855 states (over memory cap)
KLEE: WARNING: killing 12737 states (over memory cap)
KLEE: WARNING: killing 13154 states (over memory cap)
KLEE: WARNING: killing 12719 states (over memory cap)
KLEE: WARNING: killing 12386 states (over memory cap)
KLEE: WARNING: killing 12693 states (over memory cap)
KLEE: WARNING: killing 12474 states (over memory cap)
KLEE: WARNING: killing 12778 states (over memory cap)
KLEE: WARNING: killing 12873 states (over memory cap)
KLEE: WARNING: killing 12970 states (over memory cap)
KLEE: WARNING: killing 12434 states (over memory cap)
KLEE: WARNING: killing 11995 states (over memory cap)
KLEE: WARNING: killing 12831 states (over memory cap)
KLEE: WARNING: killing 12715 states (over memory cap)
KLEE: WARNING: killing 12911 states (over memory cap)
KLEE: WARNING: killing 12268 states (over memory cap)
KLEE: WARNING: killing 12681 states (over memory cap)
KLEE: WARNING: killing 12248 states (over memory cap)
KLEE: WARNING: killing 12867 states (over memory cap)
KLEE: WARNING: killing 13173 states (over memory cap)
KLEE: WARNING: killing 12843 states (over memory cap)
KLEE: WARNING: killing 12102 states (over memory cap)
KLEE: WARNING: killing 12711 states (over memory cap)
KLEE: WARNING: killing 12391 states (over memory cap)
KLEE: WARNING: killing 12999 states (over memory cap)
KLEE: WARNING: killing 12470 states (over memory cap)
KLEE: WARNING: killing 12871 states (over memory cap)
KLEE: WARNING: killing 12971 states (over memory cap)
KLEE: WARNING: killing 12439 states (over memory cap)
KLEE: WARNING: killing 12531 states (over memory cap)
KLEE: WARNING: killing 12519 states (over memory cap)
KLEE: WARNING: killing 12918 states (over memory cap)
KLEE: WARNING: killing 13321 states (over memory cap)
KLEE: WARNING: killing 13107 states (over memory cap)
KLEE: WARNING: killing 13091 states (over memory cap)
KLEE: WARNING: killing 12563 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-LzwkL4/linux-3.14__complex_emg__linux-usb-dev__drivers-net-wireless-rndis_wlan_true-unreach-call.cil.c:6739: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12758 states (over memory cap)
KLEE: WARNING: killing 12435 states (over memory cap)
KLEE: WARNING: killing 12425 states (over memory cap)
KLEE: WARNING: killing 13035 states (over memory cap)
KLEE: WARNING: killing 12918 states (over memory cap)
KLEE: WARNING: killing 12703 states (over memory cap)
KLEE: WARNING: killing 13106 states (over memory cap)
KLEE: WARNING: killing 12585 states (over memory cap)
KLEE: WARNING: killing 12570 states (over memory cap)
KLEE: WARNING: killing 12763 states (over memory cap)
KLEE: WARNING: killing 12142 states (over memory cap)
KLEE: WARNING: killing 12633 states (over memory cap)
KLEE: WARNING: killing 12832 states (over memory cap)
KLEE: WARNING: killing 12922 states (over memory cap)
KLEE: WARNING: killing 12908 states (over memory cap)
KLEE: WARNING: killing 12699 states (over memory cap)
KLEE: WARNING: killing 12281 states (over memory cap)
KLEE: WARNING: killing 12977 states (over memory cap)
KLEE: WARNING: killing 12462 states (over memory cap)
KLEE: WARNING: killing 12347 states (over memory cap)
KLEE: WARNING: killing 13045 states (over memory cap)
KLEE: WARNING: killing 12331 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-LzwkL4/linux-3.14__complex_emg__linux-usb-dev__drivers-net-wireless-rndis_wlan_true-unreach-call.cil.c:12641: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12814 states (over memory cap)
KLEE: WARNING: killing 12605 states (over memory cap)
KLEE: WARNING: killing 12586 states (over memory cap)
KLEE: WARNING: killing 12476 states (over memory cap)
KLEE: WARNING: killing 12458 states (over memory cap)
KLEE: WARNING: killing 12545 states (over memory cap)
KLEE: WARNING: killing 12234 states (over memory cap)
