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-alloc-spinlock__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.: 213 421 2509 15640
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.748576879501
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_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 'ldv_assert' (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
Defining function external_allocated_data 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
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)
Linked our definitions to these undefined functions:
  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.800927877426
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 247 315 1241 9378
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_af9fcd3d-3571-4747-a6e6-c2d16b58e023/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 15922 states (over memory cap)
KLEE: WARNING: killing 18721 states (over memory cap)
KLEE: WARNING: killing 18145 states (over memory cap)
KLEE: WARNING: killing 18568 states (over memory cap)
KLEE: WARNING: killing 18136 states (over memory cap)
KLEE: WARNING: killing 19056 states (over memory cap)
KLEE: WARNING: killing 18013 states (over memory cap)
KLEE: WARNING: killing 18681 states (over memory cap)
KLEE: WARNING: killing 18625 states (over memory cap)
KLEE: WARNING: killing 18674 states (over memory cap)
KLEE: WARNING: killing 19096 states (over memory cap)
KLEE: WARNING: killing 19406 states (over memory cap)
KLEE: WARNING: killing 19461 states (over memory cap)
KLEE: WARNING: killing 19287 states (over memory cap)
KLEE: WARNING: killing 20189 states (over memory cap)
KLEE: WARNING: killing 19660 states (over memory cap)
KLEE: WARNING: killing 19965 states (over memory cap)
KLEE: WARNING: killing 19907 states (over memory cap)
KLEE: WARNING: killing 19617 states (over memory cap)
KLEE: WARNING: killing 19455 states (over memory cap)
KLEE: WARNING: killing 19881 states (over memory cap)
KLEE: WARNING: killing 20069 states (over memory cap)
KLEE: WARNING: killing 19203 states (over memory cap)
KLEE: WARNING: killing 19155 states (over memory cap)
KLEE: WARNING: killing 19352 states (over memory cap)
KLEE: WARNING: killing 18833 states (over memory cap)
KLEE: WARNING: killing 18902 states (over memory cap)
KLEE: WARNING: killing 18514 states (over memory cap)
KLEE: WARNING: killing 18932 states (over memory cap)
KLEE: WARNING: killing 19120 states (over memory cap)
KLEE: WARNING: killing 19080 states (over memory cap)
KLEE: WARNING: killing 19725 states (over memory cap)
KLEE: WARNING: killing 19222 states (over memory cap)
KLEE: WARNING: killing 18720 states (over memory cap)
KLEE: WARNING: killing 19019 states (over memory cap)
KLEE: WARNING: killing 19315 states (over memory cap)
KLEE: WARNING: killing 18700 states (over memory cap)
KLEE: WARNING: killing 18780 states (over memory cap)
KLEE: WARNING: killing 19309 states (over memory cap)
KLEE: WARNING: killing 19384 states (over memory cap)
KLEE: WARNING: killing 18667 states (over memory cap)
KLEE: WARNING: killing 19525 states (over memory cap)
KLEE: WARNING: killing 18818 states (over memory cap)
KLEE: WARNING: killing 18769 states (over memory cap)
KLEE: WARNING: killing 18398 states (over memory cap)
KLEE: WARNING: killing 19031 states (over memory cap)
KLEE: WARNING: killing 19339 states (over memory cap)
KLEE: WARNING: killing 19190 states (over memory cap)
KLEE: WARNING: killing 19027 states (over memory cap)
KLEE: WARNING: killing 18550 states (over memory cap)
KLEE: WARNING: killing 19180 states (over memory cap)
KLEE: WARNING: killing 19134 states (over memory cap)
KLEE: WARNING: killing 19324 states (over memory cap)
KLEE: WARNING: killing 19289 states (over memory cap)
KLEE: WARNING: killing 18697 states (over memory cap)
KLEE: WARNING: killing 18762 states (over memory cap)
KLEE: WARNING: killing 19176 states (over memory cap)
KLEE: WARNING: killing 19028 states (over memory cap)
KLEE: WARNING: killing 19097 states (over memory cap)
KLEE: WARNING: killing 19071 states (over memory cap)
KLEE: WARNING: killing 19581 states (over memory cap)
KLEE: WARNING: killing 19442 states (over memory cap)
KLEE: WARNING: killing 19190 states (over memory cap)
KLEE: WARNING: killing 18492 states (over memory cap)
KLEE: WARNING: killing 18789 states (over memory cap)
KLEE: WARNING: killing 19287 states (over memory cap)
KLEE: WARNING: killing 19256 states (over memory cap)
KLEE: WARNING: killing 18677 states (over memory cap)
KLEE: WARNING: killing 18751 states (over memory cap)
KLEE: WARNING: killing 18400 states (over memory cap)
KLEE: WARNING: killing 19013 states (over memory cap)
KLEE: WARNING: killing 19189 states (over memory cap)
KLEE: WARNING: killing 19046 states (over memory cap)
KLEE: WARNING: killing 18905 states (over memory cap)
KLEE: WARNING: killing 10557 states (over memory cap)
KLEE: WARNING: killing 17686 states (over memory cap)
KLEE: WARNING: killing 18816 states (over memory cap)
KLEE: WARNING: killing 18683 states (over memory cap)
KLEE: WARNING: killing 18968 states (over memory cap)
KLEE: WARNING: killing 18936 states (over memory cap)
KLEE: WARNING: killing 10460 states (over memory cap)
KLEE: WARNING: killing 18368 states (over memory cap)
KLEE: WARNING: killing 18861 states (over memory cap)
KLEE: WARNING: killing 19363 states (over memory cap)
KLEE: WARNING: killing 18798 states (over memory cap)
KLEE: WARNING: killing 18137 states (over memory cap)
KLEE: WARNING: killing 10561 states (over memory cap)
KLEE: WARNING: killing 18507 states (over memory cap)
KLEE: WARNING: killing 18891 states (over memory cap)
KLEE: WARNING: killing 10419 states (over memory cap)
KLEE: WARNING: killing 18221 states (over memory cap)
KLEE: WARNING: killing 18709 states (over memory cap)
KLEE: WARNING: killing 10269 states (over memory cap)
KLEE: WARNING: killing 18450 states (over memory cap)
KLEE: WARNING: killing 18630 states (over memory cap)
KLEE: WARNING: killing 10331 states (over memory cap)
KLEE: WARNING: killing 18062 states (over memory cap)
KLEE: WARNING: killing 18239 states (over memory cap)
KLEE: WARNING: killing 10484 states (over memory cap)
KLEE: WARNING: killing 18713 states (over memory cap)
KLEE: WARNING: killing 18982 states (over memory cap)
KLEE: WARNING: killing 10144 states (over memory cap)
KLEE: WARNING: killing 18704 states (over memory cap)
KLEE: WARNING: killing 10206 states (over memory cap)
KLEE: WARNING: killing 18153 states (over memory cap)
KLEE: WARNING: killing 10677 states (over memory cap)
KLEE: WARNING ONCE: flushing 8280 bytes on read, may be slow and/or crash: MO1388295[8280] allocated at __VERIFIER_malloc0():  %5 = call i8* @malloc(i64 %4), !dbg !8615
KLEE: WARNING: killing 17798 states (over memory cap)
KLEE: WARNING: killing 10443 states (over memory cap)
KLEE: WARNING: killing 18262 states (over memory cap)
KLEE: WARNING: killing 10221 states (over memory cap)
KLEE: WARNING: killing 18319 states (over memory cap)
KLEE: WARNING: killing 10596 states (over memory cap)
