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-kernel-locking-mutex__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.: 198 319 2212 14167
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.604439020157
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_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.634432077408
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 238 222 1125 8237
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_caef185e-f8fc-4c66-afe7-2c426d005dfb/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 12826 states (over memory cap)
KLEE: WARNING: killing 18080 states (over memory cap)
KLEE: WARNING: killing 18492 states (over memory cap)
KLEE: WARNING: killing 18796 states (over memory cap)
KLEE: WARNING: killing 18481 states (over memory cap)
KLEE: WARNING: killing 18549 states (over memory cap)
KLEE: WARNING: killing 17744 states (over memory cap)
KLEE: WARNING: killing 17929 states (over memory cap)
KLEE: WARNING: killing 18833 states (over memory cap)
KLEE: WARNING: killing 18168 states (over memory cap)
KLEE: WARNING: killing 18951 states (over memory cap)
KLEE: WARNING: killing 19482 states (over memory cap)
KLEE: WARNING: killing 19181 states (over memory cap)
KLEE: WARNING: killing 19719 states (over memory cap)
KLEE: WARNING: killing 19899 states (over memory cap)
KLEE: WARNING: killing 19851 states (over memory cap)
KLEE: WARNING: killing 20029 states (over memory cap)
KLEE: WARNING: killing 19748 states (over memory cap)
KLEE: WARNING: killing 19704 states (over memory cap)
KLEE: WARNING: killing 19895 states (over memory cap)
KLEE: WARNING: killing 20083 states (over memory cap)
KLEE: WARNING: killing 20146 states (over memory cap)
KLEE: WARNING: killing 19631 states (over memory cap)
KLEE: WARNING: killing 20172 states (over memory cap)
KLEE: WARNING: killing 19549 states (over memory cap)
KLEE: WARNING: killing 19276 states (over memory cap)
KLEE: WARNING: killing 19353 states (over memory cap)
KLEE: WARNING: killing 18833 states (over memory cap)
KLEE: WARNING: killing 18672 states (over memory cap)
KLEE: WARNING: killing 18402 states (over memory cap)
KLEE: WARNING: killing 19151 states (over memory cap)
KLEE: WARNING: killing 18536 states (over memory cap)
KLEE: WARNING: killing 18950 states (over memory cap)
KLEE: WARNING: killing 19138 states (over memory cap)
KLEE: WARNING: killing 19326 states (over memory cap)
KLEE: WARNING: killing 19393 states (over memory cap)
KLEE: WARNING: killing 19124 states (over memory cap)
KLEE: WARNING: killing 18980 states (over memory cap)
KLEE: WARNING: killing 19393 states (over memory cap)
KLEE: WARNING: killing 19009 states (over memory cap)
KLEE: WARNING: killing 19188 states (over memory cap)
KLEE: WARNING: killing 19709 states (over memory cap)
KLEE: WARNING: killing 19232 states (over memory cap)
KLEE: WARNING: killing 18626 states (over memory cap)
KLEE: WARNING: killing 19477 states (over memory cap)
KLEE: WARNING: killing 19434 states (over memory cap)
KLEE: WARNING: killing 19847 states (over memory cap)
KLEE: WARNING: killing 19139 states (over memory cap)
KLEE: WARNING: killing 19322 states (over memory cap)
KLEE: WARNING: killing 18737 states (over memory cap)
KLEE: WARNING: killing 19356 states (over memory cap)
KLEE: WARNING: killing 19209 states (over memory cap)
KLEE: WARNING: killing 19168 states (over memory cap)
KLEE: WARNING: killing 18814 states (over memory cap)
KLEE: WARNING: killing 18556 states (over memory cap)
KLEE: WARNING: killing 18518 states (over memory cap)
KLEE: WARNING: killing 18696 states (over memory cap)
KLEE: WARNING: killing 19100 states (over memory cap)
KLEE: WARNING: killing 18959 states (over memory cap)
KLEE: WARNING: killing 19352 states (over memory cap)
KLEE: WARNING: killing 18774 states (over memory cap)
KLEE: WARNING: killing 19174 states (over memory cap)
KLEE: WARNING: killing 19682 states (over memory cap)
KLEE: WARNING: killing 18770 states (over memory cap)
KLEE: WARNING: killing 18750 states (over memory cap)
KLEE: WARNING: killing 19453 states (over memory cap)
KLEE: WARNING: killing 19536 states (over memory cap)
KLEE: WARNING: killing 18858 states (over memory cap)
KLEE: WARNING: killing 18717 states (over memory cap)
KLEE: WARNING: killing 18785 states (over memory cap)
KLEE: WARNING: killing 19500 states (over memory cap)
KLEE: WARNING: killing 18714 states (over memory cap)
KLEE: WARNING: killing 19009 states (over memory cap)
KLEE: WARNING: killing 10497 states (over memory cap)
KLEE: WARNING: killing 18214 states (over memory cap)
KLEE: WARNING: killing 19444 states (over memory cap)
KLEE: WARNING: killing 19309 states (over memory cap)
KLEE: WARNING: killing 19063 states (over memory cap)
KLEE: WARNING: killing 19025 states (over memory cap)
KLEE: WARNING: killing 19201 states (over memory cap)
KLEE: WARNING: killing 19061 states (over memory cap)
KLEE: WARNING: killing 18718 states (over memory cap)
KLEE: WARNING: killing 18782 states (over memory cap)
KLEE: WARNING: killing 18862 states (over memory cap)
KLEE: WARNING: killing 10506 states (over memory cap)
KLEE: WARNING: killing 18405 states (over memory cap)
KLEE: WARNING: killing 19195 states (over memory cap)
KLEE: WARNING: killing 18751 states (over memory cap)
KLEE: WARNING: killing 10645 states (over memory cap)
KLEE: WARNING: killing 18185 states (over memory cap)
KLEE: WARNING: killing 18867 states (over memory cap)
KLEE: WARNING: killing 18635 states (over memory cap)
KLEE: WARNING: killing 10579 states (over memory cap)
KLEE: WARNING: killing 17981 states (over memory cap)
KLEE: WARNING: killing 10352 states (over memory cap)
KLEE: WARNING: killing 18031 states (over memory cap)
KLEE: WARNING: killing 10125 states (over memory cap)
KLEE: WARNING: killing 17883 states (over memory cap)
KLEE: WARNING: killing 10502 states (over memory cap)
KLEE: WARNING: killing 17950 states (over memory cap)
KLEE: WARNING: killing 10076 states (over memory cap)
KLEE: WARNING: killing 18411 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-3eTnNQ/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-net-wireless-ath-ath10k-ath10k_pci_true-unreach-call.cil.c:7859: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10739 states (over memory cap)
KLEE: WARNING: killing 18036 states (over memory cap)
KLEE: WARNING: killing 10210 states (over memory cap)
KLEE: WARNING: killing 18190 states (over memory cap)
KLEE: WARNING: killing 10283 states (over memory cap)
KLEE: WARNING: killing 18148 states (over memory cap)
KLEE: WARNING: killing 10059 states (over memory cap)
KLEE: WARNING: killing 18192 states (over memory cap)
KLEE: WARNING: killing 10430 states (over memory cap)
KLEE: WARNING: killing 18455 states (over memory cap)
KLEE: WARNING: killing 10307 states (over memory cap)
