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--iwlwifi--dvm--iwldvm.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.: 1761 1265 12943 92443
Removed infinite loop in arch_local_save_flags___3
Removed infinite loop in arch_local_save_flags
Removed infinite loop in arch_local_save_flags___4
Removed infinite loop in arch_local_save_flags___1
Removed infinite loop in get_page
Removed infinite loop in arch_local_save_flags___2
Removed infinite loop in iwlagn_request_scan
Removed infinite loop in arch_local_save_flags___5
Removed infinite loop in arch_local_save_flags___0
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 3.04896903038
Removed calls to 'ieee80211_free_txskb' (function is undefined)
Removed calls to '__iwl_dbg' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '__iwl_warn' (function is undefined)
Removed calls to '__iwl_err' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'ieee80211_restart_hw' (function is undefined)
Removed calls to '__iwl_info' (function is undefined)
Removed calls to 'ieee80211_report_wowlan_wakeup' (function is undefined)
Removed calls to 'iwl_init_notification_wait' (function is undefined)
Removed calls to 'ieee80211_resume_disconnect' (function is undefined)
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'ieee80211_sta_block_awake' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to 'ieee80211_chswitch_done' (function is undefined)
Defining function queue_work_on as symbolic
Removed calls to 'iwl_set_bits_mask_prph' (function is undefined)
Defining function lock_is_held as symbolic
Removed calls to 'lock_release' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_watching as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Removed calls to '__raw_spin_lock_init' (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 'destroy_workqueue' (function is undefined)
Removed calls to 'ieee80211_free_hw' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Removed calls to 'iwl_notification_wait_notify' (function is undefined)
Removed calls to 'ieee80211_napi_add' (function is undefined)
Removed calls to 'ieee80211_stop_queue' (function is undefined)
Removed calls to 'ieee80211_wake_queue' (function is undefined)
Removed calls to 'wiphy_rfkill_set_hw_state' (function is undefined)
Removed calls to 'kmem_cache_free' (function is undefined)
Removed calls to 'iwl_abort_notification_waits' (function is undefined)
Removed calls to 'print_hex_dump' (function is undefined)
Defining function jiffies_to_msecs as symbolic
Defining function scnprintf as symbolic
Removed calls to 'ieee80211_unregister_hw' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'ieee80211_request_smps' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'ieee80211_disable_rssi_reports' (function is undefined)
Removed calls to 'ieee80211_enable_rssi_reports' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'iwl_remove_notification' (function is undefined)
Defining function ieee80211_beacon_get_tim as symbolic
Removed calls to 'free_pages' (function is undefined)
Defining function iwl_wait_notification as symbolic
Defining function find_first_bit as symbolic
Defining function find_next_bit as symbolic
Defining function cancel_work_sync as symbolic
Defining function del_timer_sync as symbolic
Removed calls to 'led_classdev_unregister' (function is undefined)
Defining function printk as symbolic
Defining function iwl_read_eeprom as symbolic
Defining function iwl_parse_eeprom_data as symbolic
Defining function iwl_nvm_check_version as symbolic
Removed calls to 'iwl_notification_wait_init' (function is undefined)
Defining function snprintf as symbolic
Removed calls to 'ieee80211_scan_completed' (function is undefined)
Defining function cancel_delayed_work_sync as symbolic
Defining function debugfs_create_dir as symbolic
Defining function debugfs_create_file as symbolic
Defining function debugfs_create_symlink as symbolic
Defining function ieee80211_register_hw as symbolic
Defining function kasprintf as symbolic
Defining function led_classdev_register as symbolic
Defining function __ieee80211_get_radio_led_name as symbolic
Defining function __ieee80211_create_tpt_led_trigger as symbolic
Removed calls to 'ieee80211_stop_queues' (function is undefined)
Removed calls to 'ieee80211_wake_queues' (function is undefined)
Defining function mod_timer as symbolic
Defining function __msecs_to_jiffies as symbolic
Removed calls to 'kfree_call_rcu' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'iwl_write_direct32' (function is undefined)
Removed calls to 'dump_page' (function is undefined)
Removed calls to 'skb_add_rx_frag' (function is undefined)
Removed calls to 'ieee80211_rx' (function is undefined)
Removed calls to 'ieee80211_tx_status' (function is undefined)
Defining function ieee80211_ave_rssi as symbolic
Removed calls to 'ieee80211_stop_tx_ba_cb_irqsafe' (function is undefined)
Removed calls to 'ieee80211_start_tx_ba_cb_irqsafe' (function is undefined)
Defining function ieee80211_find_sta as symbolic
Defining function ieee80211_channel_to_frequency as symbolic
Defining function skb_put as symbolic
Defining function __get_page_tail as symbolic
Defining function __alloc_skb as symbolic
Defining function __alloc_workqueue_key as symbolic
Removed calls to 'init_timer_key' (function is undefined)
Defining function queue_delayed_work_on as symbolic
Defining function cancel_delayed_work as symbolic
Removed calls to 'msleep' (function is undefined)
Defining function ieee80211_alloc_hw_nm as symbolic
Removed calls to 'debugfs_remove' (function is undefined)
Defining function debugfs_create_u8 as symbolic
Defining function rate_control_send_low as symbolic
Defining function ieee80211_start_tx_ba_session as symbolic
Defining function ieee80211_stop_tx_ba_session as symbolic
Defining function default_llseek as symbolic
Defining function simple_open as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function sscanf as symbolic
Defining function _copy_from_user as symbolic
Defining function sprintf as symbolic
Defining function simple_read_from_buffer as symbolic
Defining function generic_file_llseek as symbolic
Defining function hex_dump_to_buffer as symbolic
Removed calls to 'ieee80211_get_key_rx_seq' (function is undefined)
Removed calls to 'ieee80211_get_tkip_rx_p1k' (function is undefined)
Defining function device_set_wakeup_enable as symbolic
Removed calls to 'ieee80211_iter_keys' (function is undefined)
Removed calls to 'ieee80211_get_key_tx_seq' (function is undefined)
Removed calls to 'ieee80211_get_tkip_p1k_iv' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'ieee80211_get_tkip_p2k' (function is undefined)
Defining function rcu_read_lock_held as symbolic
Defining function pskb_expand_head as symbolic
Defining function ieee80211_hdrlen as symbolic
Defining function kmem_cache_alloc as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'iwl_opmode_deregister' (function is undefined)
Removed calls to 'ieee80211_rate_control_unregister' (function is undefined)
Defining function ldv_release_43 as symbolic
Defining function ldv_release_37 as symbolic
Defining function ldv_release_34 as symbolic
Defining function ldv_release_38 as symbolic
Defining function ldv_release_47 as symbolic
Defining function ldv_release_51 as symbolic
Defining function ldv_release_36 as symbolic
Defining function ldv_release_23 as symbolic
Defining function ldv_release_46 as symbolic
Defining function iwl_opmode_register as symbolic
Defining function ieee80211_rate_control_register as symbolic
Defining function ldv_release_42 as symbolic
Defining function ldv_release_22 as symbolic
Defining function ldv_release_53 as symbolic
Defining function ldv_release_24 as symbolic
Defining function ldv_release_49 as symbolic
Defining function ldv_release_40 as symbolic
Defining function ldv_release_28 as symbolic
Defining function ldv_release_25 as symbolic
Defining function ldv_release_30 as symbolic
Defining function ldv_release_68 as symbolic
Defining function ldv_release_67 as symbolic
Defining function ldv_release_19 as symbolic
Defining function ldv_release_45 as symbolic
Defining function ldv_release_66 as symbolic
Defining function ldv_release_52 as symbolic
Defining function ldv_release_41 as symbolic
Defining function ldv_release_39 as symbolic
Defining function ldv_release_50 as symbolic
Defining function ldv_release_29 as symbolic
Defining function ldv_release_48 as symbolic
Defining function ldv_release_35 as symbolic
Defining function ldv_release_31 as symbolic
Defining function ldv_release_20 as symbolic
Defining function ldv_release_27 as symbolic
Defining function ldv_release_44 as symbolic
Defining function ldv_release_26 as symbolic
Defining function ldv_release_21 as symbolic
Defining function ldv_release_32 as symbolic
Defining function ldv_release_33 as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  memcmp
  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: 2.92077088356
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1343 1027 7308 51663
INFO: Starting verification
KLEE: WARNING ONCE: function "iwlagn_mac_start" has inline asm
KLEE: WARNING ONCE: function "iwlagn_mac_add_interface" has inline asm
KLEE: WARNING ONCE: function "iwlagn_bss_info_changed" has inline asm
KLEE: WARNING ONCE: function "iwlagn_mac_channel_switch" has inline asm
KLEE: WARNING ONCE: function "iwl6000_nic_config" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held___3" has inline asm
KLEE: WARNING ONCE: function "iwl_op_mode_dvm_start" has inline asm
KLEE: WARNING ONCE: function "iwl_stop_sw_queue" has inline asm
KLEE: WARNING ONCE: function "iwl_wake_sw_queue" has inline asm
KLEE: WARNING ONCE: function "iwl_set_hw_rfkill_state" has inline asm
KLEE: WARNING ONCE: function "iwl_nic_error" has inline asm
KLEE: WARNING ONCE: function "iwl_wimax_active" has inline asm
KLEE: WARNING ONCE: function "iwlagn_fw_error" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held" has inline asm
KLEE: WARNING ONCE: function "iwl_write32" has inline asm
KLEE: WARNING ONCE: function "iwl_read32" has inline asm
KLEE: WARNING ONCE: function "trace_iwlwifi_dev_ucode_event" has inline asm
KLEE: WARNING ONCE: function "iwl_chswitch_done" has inline asm
KLEE: WARNING ONCE: function "iwl_power_set_mode" has inline asm
KLEE: WARNING ONCE: function "iwl_bg_restart" has inline asm
KLEE: WARNING ONCE: function "iwl_force_scan_end" has inline asm
KLEE: WARNING ONCE: function "iwl_led_cmd" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held___4" has inline asm
KLEE: WARNING ONCE: function "iwl_write32___4" has inline asm
KLEE: WARNING ONCE: function "iwl_tt_check_exit_ct_kill" has inline asm
KLEE: WARNING ONCE: function "iwl_tt_ready_for_ct_kill" has inline asm
KLEE: WARNING ONCE: function "iwl_legacy_tt_handler" has inline asm
KLEE: WARNING ONCE: function "iwl_advance_tt_handler" has inline asm
KLEE: WARNING ONCE: function "iwl_write32___1" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held___1" has inline asm
KLEE: WARNING ONCE: function "iwlagn_rx_statistics" has inline asm
KLEE: WARNING ONCE: function "iwl_rx_scan_complete_notif" has inline asm
KLEE: WARNING ONCE: function "iwlagn_rx_card_state_notif" has inline asm
KLEE: WARNING ONCE: function "iwlagn_rx_reply_rx" has inline asm
KLEE: WARNING ONCE: function "iwlagn_rx_reply_tx" has inline asm
KLEE: WARNING ONCE: function "iwlagn_check_ratid_empty" has inline asm
KLEE: WARNING ONCE: function "iwlagn_lift_passive_no_rx" has inline asm
KLEE: WARNING ONCE: function "iwl_write32___2" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held___2" has inline asm
KLEE: WARNING ONCE: function "iwl_scan_initiate" has inline asm
KLEE: WARNING ONCE: function "iwl_scan_cancel_timeout" has inline asm
KLEE: WARNING ONCE: function "iwl_process_scan_complete" has inline asm
KLEE: WARNING ONCE: function "iwl_down" has inline asm
KLEE: WARNING ONCE: function "iwl_dbgfs_power_save_status_read" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held___5" has inline asm
KLEE: WARNING ONCE: function "iwlagn_tx_agg_start" has inline asm
KLEE: WARNING ONCE: function "iwlagn_tx_agg_flush" has inline asm
KLEE: WARNING ONCE: function "iwlagn_tx_agg_stop" has inline asm
KLEE: WARNING ONCE: function "iwl_set_dynamic_key" has inline asm
KLEE: WARNING ONCE: function "iwl_remove_dynamic_key" has inline asm
KLEE: WARNING ONCE: function "iwl_get_free_ucode_key_offset" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock___0" has inline asm
KLEE: WARNING ONCE: function "iwl_write32___0" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held___0" has inline asm
KLEE: WARNING ONCE: function "iwl_load_ucode_wait_alive" has inline asm
KLEE: WARNING ONCE: function "iwl_alive_start" has inline asm
KLEE: WARNING ONCE: function "iwlagn_tx_skb" has inline asm
KLEE: WARNING ONCE: function "iwl_init_scan_params" has inline asm
KLEE: WARNING ONCE: function "iwl_bg_ucode_trace" has inline asm
KLEE: WARNING ONCE: function "trace_iwlwifi_dev_ucode_cont_event" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
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_be80c82f-a7b7-4423-a09e-cee2bc027af5/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8716 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 51541 states (over memory cap)
KLEE: WARNING: killing 42201 states (over memory cap)
KLEE: WARNING: killing 45133 states (over memory cap)
KLEE: WARNING: killing 48312 states (over memory cap)
KLEE: WARNING: killing 44802 states (over memory cap)
KLEE: WARNING: killing 47838 states (over memory cap)
KLEE: WARNING: killing 51786 states (over memory cap)
KLEE: WARNING: killing 51261 states (over memory cap)
KLEE: WARNING: killing 51116 states (over memory cap)
KLEE: WARNING: killing 48524 states (over memory cap)
KLEE: WARNING: killing 48827 states (over memory cap)
KLEE: WARNING: killing 48382 states (over memory cap)
KLEE: WARNING: killing 49054 states (over memory cap)
KLEE: WARNING: killing 48611 states (over memory cap)
KLEE: WARNING: killing 49260 states (over memory cap)
KLEE: WARNING: killing 51201 states (over memory cap)
KLEE: WARNING: killing 46096 states (over memory cap)
KLEE: WARNING: killing 47994 states (over memory cap)
KLEE: WARNING: killing 46998 states (over memory cap)
KLEE: WARNING: killing 48594 states (over memory cap)
KLEE: WARNING: killing 51944 states (over memory cap)
KLEE: WARNING: killing 50113 states (over memory cap)
KLEE: WARNING: killing 48073 states (over memory cap)
KLEE: WARNING: killing 45838 states (over memory cap)
KLEE: WARNING: killing 50566 states (over memory cap)
KLEE: WARNING: killing 46903 states (over memory cap)
KLEE: WARNING: killing 47782 states (over memory cap)
KLEE: WARNING: killing 47563 states (over memory cap)
KLEE: WARNING: killing 47726 states (over memory cap)
KLEE: WARNING: killing 50014 states (over memory cap)
KLEE: WARNING: killing 53078 states (over memory cap)
KLEE: WARNING: killing 47992 states (over memory cap)
KLEE: WARNING: killing 48134 states (over memory cap)
KLEE: WARNING: killing 43919 states (over memory cap)
KLEE: WARNING: killing 49561 states (over memory cap)
KLEE: WARNING: killing 47826 states (over memory cap)
KLEE: WARNING: killing 52527 states (over memory cap)
KLEE: WARNING: killing 49979 states (over memory cap)
KLEE: WARNING: killing 47509 states (over memory cap)
KLEE: WARNING: killing 47987 states (over memory cap)
KLEE: WARNING: killing 47902 states (over memory cap)
KLEE: WARNING: killing 48811 states (over memory cap)
KLEE: WARNING: killing 49998 states (over memory cap)
KLEE: WARNING: killing 51061 states (over memory cap)
KLEE: WARNING: killing 50105 states (over memory cap)
KLEE: WARNING: killing 50624 states (over memory cap)
KLEE: WARNING: killing 48346 states (over memory cap)
KLEE: WARNING: killing 47274 states (over memory cap)
KLEE: WARNING: killing 47988 states (over memory cap)
KLEE: WARNING: killing 50813 states (over memory cap)
KLEE: WARNING: killing 49379 states (over memory cap)
KLEE: WARNING: killing 47732 states (over memory cap)
KLEE: WARNING: killing 50325 states (over memory cap)
KLEE: WARNING: killing 50053 states (over memory cap)
KLEE: WARNING: killing 48699 states (over memory cap)
KLEE: WARNING: killing 47756 states (over memory cap)
KLEE: WARNING: killing 48008 states (over memory cap)
KLEE: WARNING: killing 48868 states (over memory cap)
KLEE: WARNING: killing 48951 states (over memory cap)
KLEE: WARNING: killing 49481 states (over memory cap)
KLEE: WARNING: killing 49413 states (over memory cap)
KLEE: WARNING: killing 51298 states (over memory cap)
KLEE: WARNING: killing 49419 states (over memory cap)
KLEE: WARNING: killing 47593 states (over memory cap)
KLEE: WARNING: killing 46440 states (over memory cap)
KLEE: WARNING: killing 50952 states (over memory cap)
KLEE: WARNING: killing 48962 states (over memory cap)
KLEE: WARNING: killing 48780 states (over memory cap)
KLEE: WARNING: killing 47728 states (over memory cap)
KLEE: WARNING: killing 50787 states (over memory cap)
KLEE: WARNING: killing 48392 states (over memory cap)
KLEE: WARNING: killing 50237 states (over memory cap)
KLEE: WARNING: killing 48672 states (over memory cap)
