bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--vfio--pci--vfio-pci.ko-main.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.: 69 157 1753 10604
INFO: Compilation, preparation and instrumentation time: 0.37629199028
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'iommu_group_put' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'pci_iounmap' (function is undefined)
Removed calls to 'pci_release_selected_regions' (function is undefined)
Removed calls to 'pci_restore_state' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'pci_unmap_rom' (function is undefined)
Defining function try_module_get as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_reset_function as symbolic
Defining function pci_save_state as symbolic
Defining function pci_store_saved_state as symbolic
Defining function pci_load_and_free_saved_state as symbolic
Defining function pci_intx_mask_supported as symbolic
Defining function pci_find_capability as symbolic
Defining function pci_bus_read_config_dword as symbolic
Defining function pci_bus_write_config_word as symbolic
Defining function pci_bus_read_config_word as symbolic
Defining function printk as symbolic
Defining function pci_bus_read_config_byte as symbolic
Defining function pci_user_write_config_word as symbolic
Defining function pci_user_write_config_byte as symbolic
Defining function pci_user_write_config_dword as symbolic
Defining function pci_user_read_config_byte as symbolic
Defining function pci_user_read_config_word as symbolic
Defining function pci_user_read_config_dword as symbolic
Removed calls to 'iowrite32' (function is undefined)
Removed calls to 'iowrite16' (function is undefined)
Removed calls to 'iowrite8' (function is undefined)
Defining function pci_request_selected_regions as symbolic
Defining function pci_iomap as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function ioread32 as symbolic
Defining function ioread16 as symbolic
Defining function ioread8 as symbolic
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Defining function pci_map_rom as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function memdup_user as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'fput' (function is undefined)
Removed calls to 'eventfd_ctx_put' (function is undefined)
Removed calls to 'pci_intx' (function is undefined)
Removed calls to 'pci_disable_msix' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Defining function eventfd_signal as symbolic
Defining function pci_enable_msix as symbolic
Defining function pci_enable_msi_block as symbolic
Removed calls to 'free_irq' (function is undefined)
Defining function kasprintf as symbolic
Defining function eventfd_ctx_fdget as symbolic
Defining function request_threaded_irq as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function queue_work as symbolic
Removed calls to 'disable_irq_nosync' (function is undefined)
Defining function pci_check_and_mask_intx as symbolic
Defining function eventfd_fget as symbolic
Defining function eventfd_ctx_fileget as symbolic
Removed calls to 'add_wait_queue' (function is undefined)
Defining function schedule_work as symbolic
Defining function eventfd_ctx_remove_wait_queue as symbolic
Defining function flush_work as symbolic
Defining function __pci_reset_function as symbolic
Defining function remap_pfn_range as symbolic
Defining function __pci_register_driver as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function vfio_del_group_dev as symbolic
Defining function iommu_group_get as symbolic
Defining function vfio_add_group_dev as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.407166004181
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 141 160 1023 6267
INFO: Starting verification
KLEE: WARNING ONCE: function "vfio_pci_release" has inline asm
KLEE: WARNING ONCE: function "vfio_pci_open" has inline asm
KLEE: WARNING ONCE: function "vfio_pci_mem_readwrite" has inline asm
KLEE: WARNING ONCE: function "vfio_pci_set_msi_trigger" has inline asm
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/symbiotic-ImPhkD/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--vfio--pci--vfio-pci.ko-main.cil.out.c:5500: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13042 states (over memory cap)
KLEE: WARNING: killing 15124 states (over memory cap)
KLEE: WARNING: killing 15288 states (over memory cap)
KLEE: WARNING: killing 14982 states (over memory cap)
KLEE: WARNING: killing 14909 states (over memory cap)
KLEE: WARNING: killing 15197 states (over memory cap)
KLEE: WARNING: killing 15478 states (over memory cap)
KLEE: WARNING: killing 15296 states (over memory cap)
KLEE: WARNING: killing 15473 states (over memory cap)
KLEE: WARNING: killing 15758 states (over memory cap)
KLEE: WARNING: killing 15817 states (over memory cap)
KLEE: WARNING: killing 15991 states (over memory cap)
KLEE: WARNING: killing 16048 states (over memory cap)
KLEE: WARNING: killing 15760 states (over memory cap)
KLEE: WARNING: killing 15813 states (over memory cap)
KLEE: WARNING: killing 16095 states (over memory cap)
KLEE: WARNING: killing 15588 states (over memory cap)
KLEE: WARNING: killing 15644 states (over memory cap)
KLEE: WARNING: killing 15702 states (over memory cap)
KLEE: WARNING: killing 15635 states (over memory cap)
KLEE: WARNING: killing 15807 states (over memory cap)
KLEE: WARNING: killing 15643 states (over memory cap)
KLEE: WARNING: killing 15808 states (over memory cap)
KLEE: WARNING: killing 15535 states (over memory cap)
KLEE: WARNING: killing 15482 states (over memory cap)
KLEE: WARNING: killing 15537 states (over memory cap)
KLEE: WARNING: killing 15370 states (over memory cap)
KLEE: WARNING: killing 15318 states (over memory cap)
KLEE: WARNING: killing 15595 states (over memory cap)
KLEE: WARNING: killing 15763 states (over memory cap)
KLEE: WARNING: killing 15604 states (over memory cap)
KLEE: WARNING: killing 15768 states (over memory cap)
KLEE: WARNING: killing 15830 states (over memory cap)
KLEE: WARNING: killing 15671 states (over memory cap)
KLEE: WARNING: killing 15416 states (over memory cap)
KLEE: WARNING: killing 15577 states (over memory cap)
KLEE: WARNING: killing 15633 states (over memory cap)
KLEE: WARNING: killing 15692 states (over memory cap)
KLEE: WARNING: killing 15541 states (over memory cap)
KLEE: WARNING: killing 15699 states (over memory cap)
KLEE: WARNING: killing 15545 states (over memory cap)
KLEE: WARNING: killing 15505 states (over memory cap)
KLEE: WARNING: killing 15453 states (over memory cap)
KLEE: WARNING: killing 15407 states (over memory cap)
KLEE: WARNING: killing 15669 states (over memory cap)
KLEE: WARNING: killing 15417 states (over memory cap)
KLEE: WARNING: killing 15469 states (over memory cap)
KLEE: WARNING: killing 15318 states (over memory cap)
KLEE: WARNING: killing 15687 states (over memory cap)
KLEE: WARNING: killing 15548 states (over memory cap)
KLEE: WARNING: killing 15300 states (over memory cap)
KLEE: WARNING: killing 15356 states (over memory cap)
KLEE: WARNING: killing 15416 states (over memory cap)
KLEE: WARNING: killing 15777 states (over memory cap)
KLEE: WARNING: killing 15637 states (over memory cap)
KLEE: WARNING: killing 15696 states (over memory cap)
KLEE: WARNING: killing 15452 states (over memory cap)
KLEE: WARNING: killing 15308 states (over memory cap)
KLEE: WARNING: killing 15274 states (over memory cap)
KLEE: WARNING: killing 15627 states (over memory cap)
KLEE: WARNING: killing 15586 states (over memory cap)
KLEE: WARNING: killing 15546 states (over memory cap)
KLEE: WARNING: killing 15213 states (over memory cap)
KLEE: WARNING: killing 15472 states (over memory cap)
KLEE: WARNING: killing 15329 states (over memory cap)
KLEE: WARNING: killing 15190 states (over memory cap)
KLEE: WARNING: killing 15347 states (over memory cap)
KLEE: WARNING: killing 15498 states (over memory cap)
KLEE: WARNING: killing 15163 states (over memory cap)
KLEE: WARNING: killing 15124 states (over memory cap)
KLEE: WARNING: killing 15284 states (over memory cap)
KLEE: WARNING: killing 15440 states (over memory cap)
KLEE: WARNING: killing 15307 states (over memory cap)
KLEE: WARNING: killing 15665 states (over memory cap)
KLEE: WARNING: killing 15433 states (over memory cap)
KLEE: WARNING: killing 15204 states (over memory cap)
KLEE: WARNING: killing 15451 states (over memory cap)
KLEE: WARNING: killing 15610 states (over memory cap)
KLEE: WARNING: killing 15289 states (over memory cap)
KLEE: WARNING: killing 15542 states (over memory cap)
KLEE: WARNING: killing 15605 states (over memory cap)
KLEE: WARNING: killing 15181 states (over memory cap)
KLEE: WARNING: killing 15237 states (over memory cap)
KLEE: WARNING: killing 15296 states (over memory cap)
KLEE: WARNING: killing 15258 states (over memory cap)
KLEE: WARNING: killing 15129 states (over memory cap)
KLEE: WARNING: killing 15377 states (over memory cap)
KLEE: WARNING: killing 15348 states (over memory cap)
KLEE: WARNING: killing 15309 states (over memory cap)
KLEE: WARNING: killing 15278 states (over memory cap)
KLEE: WARNING: killing 15335 states (over memory cap)
KLEE: WARNING: killing 15392 states (over memory cap)
KLEE: WARNING: killing 14979 states (over memory cap)
KLEE: WARNING: killing 15316 states (over memory cap)
KLEE: WARNING: killing 15278 states (over memory cap)
KLEE: WARNING: killing 15349 states (over memory cap)
KLEE: WARNING: killing 15398 states (over memory cap)
KLEE: WARNING: killing 15186 states (over memory cap)
KLEE: WARNING: killing 15061 states (over memory cap)
