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--ti--wl12xx--wl12xx.ko-entry_point_false-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.: 620 437 4587 24675
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.03738808632
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'wlcore_enable_interrupts' (function is undefined)
Removed calls to 'wlcore_disable_interrupts' (function is undefined)
Removed calls to 'wlcore_scan_sched_scan_results' (function is undefined)
Removed calls to 'wlcore_event_sched_scan_completed' (function is undefined)
Removed calls to 'wlcore_event_soft_gemini_sense' (function is undefined)
Removed calls to 'wlcore_event_beacon_loss' (function is undefined)
Removed calls to 'wlcore_event_rssi_trigger' (function is undefined)
Removed calls to 'wlcore_event_ba_rx_constraint' (function is undefined)
Removed calls to 'wlcore_event_channel_switch' (function is undefined)
Removed calls to 'wlcore_event_dummy_packet' (function is undefined)
Removed calls to 'wlcore_event_max_tx_failure' (function is undefined)
Removed calls to 'wlcore_event_inactive_sta' (function is undefined)
Removed calls to 'wlcore_event_roc_complete' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function wl1271_acx_set_ht_capabilities as symbolic
Defining function wl1271_cmd_send as symbolic
Defining function printk as symbolic
Defining function wlcore_set_key as symbolic
Defining function wlcore_scan_sched_scan_ssid_list as symbolic
Defining function wlcore_set_scan_chan_params as symbolic
Defining function wl12xx_cmd_build_probe_req as symbolic
Removed calls to 'ieee80211_queue_delayed_work' (function is undefined)
Defining function wl1271_tx_min_rate_get as symbolic
Defining function cancel_delayed_work as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function debugfs_create_dir as symbolic
Defining function debugfs_create_file as symbolic
Defining function wlcore_set_partition as symbolic
Defining function wlcore_translate_addr as symbolic
Defining function wl1271_cmd_test as symbolic
Defining function wl1271_cmd_configure as symbolic
Defining function wlcore_tx_complete as symbolic
Defining function wlcore_calc_packet_alignment as symbolic
Defining function wlcore_cmd_wait_for_event_or_timeout as symbolic
Defining function wl1271_acx_init_mem_config as symbolic
Defining function wl12xx_acx_mem_cfg as symbolic
Defining function wl1271_cmd_data_path as symbolic
Defining function wl1271_acx_sleep_auth as symbolic
Defining function wl1271_acx_pm_config as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Defining function wlcore_boot_upload_nvs as symbolic
Defining function wlcore_boot_upload_firmware as symbolic
Defining function wlcore_boot_run_firmware as symbolic
Defining function __usecs_to_jiffies as symbolic
Defining function wlcore_remove as symbolic
Defining function wlcore_alloc_hw as symbolic
Defining function wlcore_free_hw as symbolic
Defining function wlcore_probe as symbolic
Defining function generic_file_llseek as symbolic
Removed calls to 'wl1271_debugfs_update_stats' (function is undefined)
Defining function simple_open as symbolic
Defining function wl1271_format_buffer as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'platform_driver_unregister' (function is undefined)
Defining function ldv_release_80 as symbolic
Defining function ldv_init_80 as symbolic
Defining function ldv_release_5 as symbolic
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_4 as symbolic
Defining function ldv_release_38 as symbolic
Defining function ldv_release_8 as symbolic
Defining function ldv_release_47 as symbolic
Defining function ldv_release_51 as symbolic
Defining function ldv_release_9 as symbolic
Defining function ldv_release_36 as symbolic
Defining function ldv_release_3 as symbolic
Defining function ldv_release_6 as symbolic
Defining function ldv_release_13 as symbolic
Defining function ldv_release_23 as symbolic
Defining function ldv_release_46 as symbolic
Defining function __platform_driver_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_59 as symbolic
Defining function ldv_release_69 as symbolic
Defining function ldv_release_14 as symbolic
Defining function ldv_release_40 as symbolic
Defining function ldv_release_75 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_1 as symbolic
Defining function ldv_release_17 as symbolic
Defining function ldv_release_2 as symbolic
Defining function ldv_release_68 as symbolic
Defining function ldv_release_70 as symbolic
Defining function ldv_release_67 as symbolic
Defining function ldv_release_54 as symbolic
Defining function ldv_release_62 as symbolic
Defining function ldv_release_19 as symbolic
Defining function ldv_release_76 as symbolic
Defining function ldv_release_45 as symbolic
Defining function ldv_release_66 as symbolic
Defining function ldv_release_73 as symbolic
Defining function ldv_release_56 as symbolic
Defining function ldv_release_60 as symbolic
Defining function ldv_release_52 as symbolic
Defining function ldv_release_15 as symbolic
Defining function ldv_release_12 as symbolic
Defining function ldv_release_41 as symbolic
Defining function ldv_release_58 as symbolic
Defining function ldv_release_64 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_65 as symbolic
Defining function ldv_release_77 as symbolic
Defining function ldv_release_48 as symbolic
Defining function ldv_release_78 as symbolic
Defining function ldv_release_11 as symbolic
Defining function ldv_release_35 as symbolic
Defining function ldv_release_31 as symbolic
Defining function ldv_release_10 as symbolic
Defining function ldv_release_20 as symbolic
Defining function ldv_release_61 as symbolic
Defining function ldv_release_57 as symbolic
Defining function ldv_release_27 as symbolic
Defining function ldv_release_74 as symbolic
Defining function ldv_release_55 as symbolic
Defining function ldv_release_44 as symbolic
Defining function ldv_release_16 as symbolic
Defining function ldv_release_72 as symbolic
Defining function ldv_release_18 as symbolic
Defining function ldv_release_26 as symbolic
Defining function ldv_release_7 as symbolic
Defining function ldv_release_71 as symbolic
Defining function ldv_release_21 as symbolic
Defining function ldv_release_63 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:
  strcmp
  __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.92283987999
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 721 524 2486 16194
INFO: Starting verification
KLEE: WARNING ONCE: function "wl12xx_lnk_high_prio" has inline asm
KLEE: WARNING ONCE: function "wl1271_scan_send" has inline asm
KLEE: WARNING ONCE: function "wlcore_raw_read32" has inline asm
KLEE: WARNING ONCE: function "wlcore_raw_write" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
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_61a07640-ad67-4ca8-a109-43680d600302/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12430 states (over memory cap)
KLEE: WARNING: killing 63254 states (over memory cap)
KLEE: WARNING: killing 58355 states (over memory cap)
KLEE: WARNING: killing 57930 states (over memory cap)
KLEE: WARNING: killing 54781 states (over memory cap)
KLEE: WARNING: killing 53971 states (over memory cap)
KLEE: WARNING: killing 59016 states (over memory cap)
KLEE: WARNING: killing 67267 states (over memory cap)
KLEE: WARNING: killing 65761 states (over memory cap)
KLEE: WARNING: killing 66287 states (over memory cap)
KLEE: WARNING: killing 65785 states (over memory cap)
KLEE: WARNING: killing 66146 states (over memory cap)
KLEE: WARNING: killing 61212 states (over memory cap)
KLEE: WARNING: killing 63167 states (over memory cap)
KLEE: WARNING: killing 62000 states (over memory cap)
KLEE: WARNING: killing 61197 states (over memory cap)
KLEE: WARNING: killing 61842 states (over memory cap)
KLEE: WARNING: killing 62135 states (over memory cap)
KLEE: WARNING: killing 63508 states (over memory cap)
KLEE: WARNING: killing 65366 states (over memory cap)
KLEE: WARNING: killing 63297 states (over memory cap)
KLEE: WARNING: killing 62693 states (over memory cap)
KLEE: WARNING: killing 64550 states (over memory cap)
KLEE: WARNING: killing 63389 states (over memory cap)
KLEE: WARNING: killing 62280 states (over memory cap)
KLEE: WARNING: killing 67282 states (over memory cap)
KLEE: WARNING: killing 63142 states (over memory cap)
KLEE: WARNING: killing 61792 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 64360 states (over memory cap)
KLEE: WARNING: killing 67141 states (over memory cap)
KLEE: WARNING: killing 62289 states (over memory cap)
KLEE: WARNING: killing 63784 states (over memory cap)
KLEE: WARNING: killing 68128 states (over memory cap)
KLEE: WARNING: killing 63477 states (over memory cap)
KLEE: WARNING: killing 61922 states (over memory cap)
KLEE: WARNING: killing 64939 states (over memory cap)
KLEE: WARNING: killing 62324 states (over memory cap)
KLEE: WARNING: killing 62615 states (over memory cap)
KLEE: WARNING: killing 62779 states (over memory cap)
KLEE: WARNING: killing 62378 states (over memory cap)
KLEE: WARNING: killing 66819 states (over memory cap)
KLEE: WARNING: killing 65117 states (over memory cap)
KLEE: WARNING: killing 61426 states (over memory cap)
KLEE: WARNING: killing 66317 states (over memory cap)
KLEE: WARNING: killing 61176 states (over memory cap)
KLEE: WARNING: killing 61105 states (over memory cap)
KLEE: WARNING: killing 63091 states (over memory cap)
KLEE: WARNING: killing 65166 states (over memory cap)
KLEE: WARNING: killing 63473 states (over memory cap)
KLEE: WARNING: killing 65299 states (over memory cap)
KLEE: WARNING: killing 65291 states (over memory cap)
KLEE: WARNING: killing 63334 states (over memory cap)
KLEE: WARNING: killing 59765 states (over memory cap)
KLEE: WARNING: killing 60915 states (over memory cap)
KLEE: WARNING: killing 68072 states (over memory cap)
KLEE: WARNING: killing 62404 states (over memory cap)
KLEE: WARNING: killing 60918 states (over memory cap)
KLEE: WARNING: killing 65612 states (over memory cap)
KLEE: WARNING: killing 64672 states (over memory cap)
KLEE: WARNING: killing 62148 states (over memory cap)
KLEE: WARNING: killing 64347 states (over memory cap)
KLEE: WARNING: killing 64929 states (over memory cap)
KLEE: WARNING: killing 64163 states (over memory cap)
KLEE: WARNING: killing 63754 states (over memory cap)
KLEE: WARNING: killing 61012 states (over memory cap)
KLEE: WARNING: killing 65907 states (over memory cap)
KLEE: WARNING: killing 58223 states (over memory cap)
KLEE: WARNING: killing 66093 states (over memory cap)
KLEE: WARNING: killing 63687 states (over memory cap)
