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-drivers-clk1__drivers-net-wireless-ath-ath10k-ath10k_pci_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.: 196 299 2144 13798
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.571170091629
Removed calls to '__tasklet_schedule' (function is undefined)
Removed calls to 'iowrite32' (function is undefined)
Defining function ioread32 as symbolic
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function ath10k_err as symbolic
Defining function __pci_register_driver as symbolic
Defining function ath10k_warn as symbolic
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function kmemdup as symbolic
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to 'debug_dma_mapping_error' (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 'debug_dma_unmap_page' (function is undefined)
Defining function completion_done as symbolic
Removed calls to '__udelay' (function is undefined)
Defining function __phys_addr as symbolic
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'tasklet_kill' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Removed calls to 'tasklet_init' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function ath10k_info as symbolic
Removed calls to 'ath10k_dbg' (function is undefined)
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Defining function request_threaded_irq as symbolic
Defining function pci_enable_msi_block as symbolic
Defining function queue_work_on as symbolic
Removed calls to 'ath10k_dbg_dump' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'pci_iounmap' (function is undefined)
Removed calls to 'pci_clear_master' (function is undefined)
Removed calls to 'pci_release_region' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'ath10k_core_destroy' (function is undefined)
Removed calls to 'ath10k_core_unregister' (function is undefined)
Defining function ath10k_core_create as symbolic
Defining function pci_assign_resource as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_request_region as symbolic
Defining function pci_iomap as symbolic
Defining function ath10k_core_register as symbolic
Defining function pci_bus_write_config_dword as symbolic
Defining function pci_bus_read_config_dword as symbolic
Defining function dma_supported as symbolic
Defining function dma_set_mask as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to 'pci_restore_state' (function is undefined)
Defining function pci_save_state as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to 'skb_trim' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'debug_dma_sync_single_for_device' (function is undefined)
Defining function skb_put as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'ldv_initialize' (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 'ldv_pre_probe' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  __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.566667079926
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 236 202 1049 7974
INFO: Starting verification
KLEE: WARNING ONCE: function "dma_map_single_attrs" has inline asm
KLEE: WARNING ONCE: function "dma_unmap_single_attrs" has inline asm
KLEE: WARNING ONCE: function "ath10k_do_pci_wake" has inline asm
KLEE: WARNING ONCE: function "pci_free_consistent" has inline asm
KLEE: WARNING ONCE: function "ath10k_ce_init" has inline asm
KLEE: WARNING ONCE: function "ath10k_pci_probe" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_40ba5129-fafb-40f4-aea1-b14d4eb830e1/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 13125 states (over memory cap)
KLEE: WARNING: killing 18225 states (over memory cap)
KLEE: WARNING: killing 18649 states (over memory cap)
KLEE: WARNING: killing 18703 states (over memory cap)
KLEE: WARNING: killing 17791 states (over memory cap)
KLEE: WARNING: killing 17612 states (over memory cap)
KLEE: WARNING: killing 18144 states (over memory cap)
KLEE: WARNING: killing 18445 states (over memory cap)
KLEE: WARNING: killing 18866 states (over memory cap)
KLEE: WARNING: killing 18328 states (over memory cap)
KLEE: WARNING: killing 18742 states (over memory cap)
KLEE: WARNING: killing 18917 states (over memory cap)
KLEE: WARNING: killing 19696 states (over memory cap)
KLEE: WARNING: killing 20112 states (over memory cap)
KLEE: WARNING: killing 19942 states (over memory cap)
KLEE: WARNING: killing 20474 states (over memory cap)
KLEE: WARNING: killing 20421 states (over memory cap)
KLEE: WARNING: killing 20019 states (over memory cap)
KLEE: WARNING: killing 19844 states (over memory cap)
KLEE: WARNING: killing 19919 states (over memory cap)
KLEE: WARNING: killing 19640 states (over memory cap)
KLEE: WARNING: killing 19245 states (over memory cap)
KLEE: WARNING: killing 19899 states (over memory cap)
KLEE: WARNING: killing 19501 states (over memory cap)
KLEE: WARNING: killing 19342 states (over memory cap)
KLEE: WARNING: killing 19182 states (over memory cap)
KLEE: WARNING: killing 18679 states (over memory cap)
KLEE: WARNING: killing 19546 states (over memory cap)
KLEE: WARNING: killing 19168 states (over memory cap)
KLEE: WARNING: killing 18657 states (over memory cap)
KLEE: WARNING: killing 19194 states (over memory cap)
KLEE: WARNING: killing 19033 states (over memory cap)
KLEE: WARNING: killing 18998 states (over memory cap)
KLEE: WARNING: killing 19175 states (over memory cap)
KLEE: WARNING: killing 18792 states (over memory cap)
KLEE: WARNING: killing 18975 states (over memory cap)
KLEE: WARNING: killing 18930 states (over memory cap)
KLEE: WARNING: killing 19561 states (over memory cap)
KLEE: WARNING: killing 18958 states (over memory cap)
KLEE: WARNING: killing 19035 states (over memory cap)
KLEE: WARNING: killing 19336 states (over memory cap)
KLEE: WARNING: killing 19626 states (over memory cap)
KLEE: WARNING: killing 19034 states (over memory cap)
KLEE: WARNING: killing 18996 states (over memory cap)
KLEE: WARNING: killing 18964 states (over memory cap)
KLEE: WARNING: killing 19584 states (over memory cap)
KLEE: WARNING: killing 18772 states (over memory cap)
KLEE: WARNING: killing 19389 states (over memory cap)
KLEE: WARNING: killing 19250 states (over memory cap)
KLEE: WARNING: killing 18992 states (over memory cap)
KLEE: WARNING: killing 19503 states (over memory cap)
KLEE: WARNING: killing 18702 states (over memory cap)
KLEE: WARNING: killing 19100 states (over memory cap)
KLEE: WARNING: killing 18625 states (over memory cap)
KLEE: WARNING: killing 19022 states (over memory cap)
KLEE: WARNING: killing 19754 states (over memory cap)
KLEE: WARNING: killing 19385 states (over memory cap)
KLEE: WARNING: killing 19349 states (over memory cap)
KLEE: WARNING: killing 19722 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-XDozez/linux-3.14__complex_emg__linux-drivers-clk1__drivers-net-wireless-ath-ath10k-ath10k_pci_true-unreach-call.cil.c:7857: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 18822 states (over memory cap)
KLEE: WARNING: killing 18995 states (over memory cap)
KLEE: WARNING: killing 19068 states (over memory cap)
KLEE: WARNING: killing 18934 states (over memory cap)
KLEE: WARNING: killing 18578 states (over memory cap)
KLEE: WARNING: killing 18646 states (over memory cap)
KLEE: WARNING: killing 18821 states (over memory cap)
KLEE: WARNING: killing 18894 states (over memory cap)
KLEE: WARNING: killing 19075 states (over memory cap)
KLEE: WARNING: killing 18940 states (over memory cap)
KLEE: WARNING: killing 18581 states (over memory cap)
KLEE: WARNING: killing 18967 states (over memory cap)
KLEE: WARNING: killing 19249 states (over memory cap)
KLEE: WARNING: killing 18586 states (over memory cap)
KLEE: WARNING: killing 18869 states (over memory cap)
KLEE: WARNING: killing 10734 states (over memory cap)
KLEE: WARNING: killing 18819 states (over memory cap)
KLEE: WARNING: killing 10499 states (over memory cap)
KLEE: WARNING: killing 18568 states (over memory cap)
KLEE: WARNING: killing 10369 states (over memory cap)
KLEE: WARNING: killing 18735 states (over memory cap)
KLEE: WARNING: killing 19024 states (over memory cap)
KLEE: WARNING: killing 10332 states (over memory cap)
KLEE: WARNING: killing 18773 states (over memory cap)
KLEE: WARNING: killing 18628 states (over memory cap)
KLEE: WARNING: killing 19110 states (over memory cap)
KLEE: WARNING: killing 10579 states (over memory cap)
KLEE: WARNING: killing 18456 states (over memory cap)
KLEE: WARNING: killing 10244 states (over memory cap)
KLEE: WARNING: killing 18093 states (over memory cap)
KLEE: WARNING: killing 10214 states (over memory cap)
KLEE: WARNING: killing 17738 states (over memory cap)
KLEE: WARNING: killing 10286 states (over memory cap)
KLEE: WARNING: killing 17790 states (over memory cap)
KLEE: WARNING: killing 10160 states (over memory cap)
KLEE: WARNING: killing 17843 states (over memory cap)
KLEE: WARNING: killing 10334 states (over memory cap)
KLEE: WARNING: killing 18408 states (over memory cap)
KLEE: WARNING: killing 10407 states (over memory cap)
KLEE: WARNING: killing 18465 states (over memory cap)
KLEE: WARNING: killing 10280 states (over memory cap)
KLEE: WARNING: killing 18414 states (over memory cap)
KLEE: WARNING: killing 10555 states (over memory cap)
KLEE: WARNING: killing 18066 states (over memory cap)
KLEE: WARNING: killing 10424 states (over memory cap)
KLEE: WARNING: killing 18425 states (over memory cap)
KLEE: WARNING: killing 10500 states (over memory cap)
KLEE: WARNING: killing 18577 states (over memory cap)
KLEE: WARNING: killing 10472 states (over memory cap)
KLEE: WARNING: killing 17930 states (over memory cap)
KLEE: WARNING: killing 10346 states (over memory cap)
