bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--mwifiex--mwifiex_sdio.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.: 159 95 1175 8111
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.389148950577
Removed calls to 'mmc_remove_host' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function printk as symbolic
Defining function mmc_add_host as symbolic
Removed calls to 'sdio_claim_host' (function is undefined)
Removed calls to 'sdio_release_host' (function is undefined)
Removed calls to 'mwifiex_deauthenticate_all' (function is undefined)
Defining function mwifiex_disable_auto_ds as symbolic
Defining function mwifiex_init_shutdown_fw as symbolic
Defining function mwifiex_remove_card as symbolic
Defining function sdio_get_host_pm_caps as symbolic
Defining function dev_warn as symbolic
Defining function mwifiex_cancel_hs as symbolic
Defining function sdio_enable_func as symbolic
Defining function mwifiex_add_card as symbolic
Defining function sdio_disable_func as symbolic
Defining function mwifiex_enable_hs as symbolic
Defining function dev_err as symbolic
Defining function sdio_set_host_pm_flags as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to 'usleep_range' (function is undefined)
Removed calls to 'sdio_writeb' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to 'skb_trim' (function is undefined)
Defining function queue_work_on as symbolic
Defining function sdio_writesb as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function skb_put as symbolic
Removed calls to 'mwifiex_process_sleep_confirm_resp' (function is undefined)
Defining function sdio_readb as symbolic
Defining function sdio_readsb as symbolic
Defining function skb_pull as symbolic
Defining function mwifiex_handle_rx_packet as symbolic
Defining function sdio_release_irq as symbolic
Defining function sdio_claim_irq as symbolic
Defining function mwifiex_main_process as symbolic
Defining function sdio_set_block_size as symbolic
Removed calls to 'up' (function is undefined)
Removed calls to 'sdio_unregister_driver' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Defining function ldv_suspend_late_4 as symbolic
Defining function ldv_resume_early_4 as symbolic
Defining function ldv_resume_noirq_4 as symbolic
Defining function ldv_prepare_4 as symbolic
Defining function ldv_suspend_noirq_4 as symbolic
Defining function ldv_complete_4 as symbolic
Defining function sdio_register_driver as symbolic
Defining function down_interruptible as symbolic
Defining function cancel_work_sync as symbolic
Linked our definitions to these undefined functions:
  strcpy
  __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_u32_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.39325094223
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 187 111 602 4581
INFO: Starting verification
KLEE: WARNING: undefined reference to function: __VERIFIER_nondet_u16_named
KLEE: WARNING: undefined reference to function: __VERIFIER_nondet_u8_named
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-7qfww4/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING: undefined reference to function: __VERIFIER_nondet_u16_named
KLEE: WARNING: undefined reference to function: __VERIFIER_nondet_u8_named
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 0.912643909454
