bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-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.: 101 255 2409 13836
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 3.35389208794
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 'vga_set_legacy_decoding' (function is undefined)
Defining function vfio_del_group_dev as symbolic
Defining function vga_client_register as symbolic
Defining function pci_set_power_state as symbolic
Defining function iommu_group_get as symbolic
Defining function vfio_add_group_dev as symbolic
Removed calls to 'vfio_device_put' (function is undefined)
Defining function vfio_device_get_from_dev as symbolic
Defining function vfio_device_data as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Defining function eventfd_signal as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'pci_clear_master' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'module_put' (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 'pci_walk_bus' (function is undefined)
Removed calls to 'pci_unmap_rom' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'fput' (function is undefined)
Removed calls to 'vfio_group_put_external_user' (function is undefined)
Removed calls to 'dev_notice' (function is undefined)
Removed calls to 'dev_warn' (function is undefined)
Defining function ___ratelimit as symbolic
Defining function pci_request_selected_regions as symbolic
Defining function pci_iomap as symbolic
Defining function remap_pfn_range as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function pci_map_rom as symbolic
Defining function memdup_user as symbolic
Defining function pci_try_reset_function as symbolic
Defining function pci_probe_reset_slot as symbolic
Defining function pci_probe_reset_bus as symbolic
Defining function vfio_group_get_external_user as symbolic
Defining function vfio_external_user_iommu_id as symbolic
Defining function pci_try_reset_slot as symbolic
Defining function pci_try_reset_bus as symbolic
Defining function iommu_group_id as symbolic
Defining function __fdget as symbolic
Removed calls to 'vfio_virqfd_disable' (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)
Removed calls to 'eventfd_ctx_put' (function is undefined)
Defining function eventfd_ctx_fdget as symbolic
Defining function pci_enable_msix_range as symbolic
Defining function pci_enable_msi_range as symbolic
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'get_cached_msi_msg' (function is undefined)
Removed calls to 'pci_write_msi_msg' (function is undefined)
Defining function kasprintf as symbolic
Removed calls to 'disable_irq_nosync' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function pci_check_and_mask_intx as symbolic
Defining function request_threaded_irq as symbolic
Removed calls to 'enable_irq' (function is undefined)
Defining function vfio_virqfd_enable as symbolic
Defining function pci_check_and_unmask_intx as symbolic
Defining function pci_bus_read_config_word as symbolic
Defining function pci_bus_read_config_byte as symbolic
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Removed calls to 'ioport_unmap' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'vga_put' (function is undefined)
Defining function ioremap_nocache as symbolic
Defining function ioport_map 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 ioread32 as symbolic
Defining function ioread16 as symbolic
Defining function ioread8 as symbolic
Defining function vga_get as symbolic
Defining function pci_load_and_free_saved_state as symbolic
Defining function printk as symbolic
Defining function pci_save_state as symbolic
Defining function pci_dev_driver as symbolic
Defining function pci_bus_write_config_word as symbolic
Defining function try_module_get as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_reset_function as symbolic
Defining function pci_store_saved_state as symbolic
Defining function pci_intx_mask_supported as symbolic
Defining function pci_bus_read_config_dword 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 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function ldv_shutdown_4 as symbolic
Defining function ldv_release_3 as symbolic
Defining function ldv_probe_3 as symbolic
Defining function sscanf as symbolic
Defining function pci_add_dynid as symbolic
Defining function strsep as symbolic
Defining function __pci_register_driver as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  strlen
  __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: 2.63845682144
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 204 264 1485 8248
INFO: Starting verification
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/vcloud-vcloud-master/worker/working_dir_4942fb72-e3f4-4521-8159-adb2c6fb7903/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-o3uqmU/linux-4.2-rc1.tar.xz-32_7a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139734: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16994 states (over memory cap)
KLEE: WARNING: killing 10936 states (over memory cap)
KLEE: WARNING: killing 10150 states (over memory cap)
KLEE: WARNING: killing 10211 states (over memory cap)
KLEE: WARNING: killing 9850 states (over memory cap)
KLEE: WARNING: killing 10074 states (over memory cap)
KLEE: WARNING: killing 10136 states (over memory cap)
KLEE: WARNING: killing 10196 states (over memory cap)
KLEE: WARNING: killing 10336 states (over memory cap)
KLEE: WARNING: killing 10315 states (over memory cap)
KLEE: WARNING: killing 10625 states (over memory cap)
KLEE: WARNING: killing 10687 states (over memory cap)
KLEE: WARNING: killing 10667 states (over memory cap)
KLEE: WARNING: killing 11062 states (over memory cap)
KLEE: WARNING: killing 11452 states (over memory cap)
KLEE: WARNING: killing 11353 states (over memory cap)
KLEE: WARNING: killing 11582 states (over memory cap)
KLEE: WARNING: killing 11322 states (over memory cap)
KLEE: WARNING: killing 11226 states (over memory cap)
KLEE: WARNING: killing 11124 states (over memory cap)
KLEE: WARNING: killing 10943 states (over memory cap)
KLEE: WARNING: killing 10931 states (over memory cap)
KLEE: WARNING: killing 11079 states (over memory cap)
KLEE: WARNING: killing 11225 states (over memory cap)
KLEE: WARNING: killing 10886 states (over memory cap)
KLEE: WARNING: killing 10785 states (over memory cap)
KLEE: WARNING: killing 10443 states (over memory cap)
KLEE: WARNING: killing 10022 states (over memory cap)
KLEE: WARNING: killing 10487 states (over memory cap)
KLEE: WARNING: killing 10552 states (over memory cap)
KLEE: WARNING: killing 10617 states (over memory cap)
KLEE: WARNING: killing 10523 states (over memory cap)
KLEE: WARNING: killing 10666 states (over memory cap)
KLEE: WARNING: killing 10890 states (over memory cap)
KLEE: WARNING: killing 10474 states (over memory cap)
KLEE: WARNING: killing 10376 states (over memory cap)
KLEE: WARNING: killing 10438 states (over memory cap)
KLEE: WARNING: killing 10905 states (over memory cap)
KLEE: WARNING: killing 11049 states (over memory cap)
KLEE: WARNING: killing 10397 states (over memory cap)
KLEE: WARNING: killing 10856 states (over memory cap)
KLEE: WARNING: killing 10526 states (over memory cap)
KLEE: WARNING: killing 10745 states (over memory cap)
KLEE: WARNING: killing 10813 states (over memory cap)
KLEE: WARNING: killing 10880 states (over memory cap)
KLEE: WARNING: killing 11024 states (over memory cap)
KLEE: WARNING: killing 10929 states (over memory cap)
KLEE: WARNING: killing 10683 states (over memory cap)
KLEE: WARNING: killing 10589 states (over memory cap)
KLEE: WARNING: killing 10970 states (over memory cap)
KLEE: WARNING: killing 10723 states (over memory cap)
KLEE: WARNING: killing 10551 states (over memory cap)
KLEE: WARNING: killing 11006 states (over memory cap)
KLEE: WARNING: killing 10523 states (over memory cap)
KLEE: WARNING: killing 10434 states (over memory cap)
KLEE: WARNING: killing 10734 states (over memory cap)
KLEE: WARNING: killing 10564 states (over memory cap)
KLEE: WARNING: killing 10706 states (over memory cap)
KLEE: WARNING: killing 10463 states (over memory cap)
KLEE: WARNING: killing 10757 states (over memory cap)
KLEE: WARNING: killing 10280 states (over memory cap)
KLEE: WARNING: killing 10964 states (over memory cap)
KLEE: WARNING: killing 10175 states (over memory cap)
KLEE: WARNING: killing 10626 states (over memory cap)
KLEE: WARNING: killing 10846 states (over memory cap)
KLEE: WARNING: killing 10759 states (over memory cap)
KLEE: WARNING: killing 10822 states (over memory cap)
KLEE: WARNING: killing 10888 states (over memory cap)
KLEE: WARNING: killing 10719 states (over memory cap)
KLEE: WARNING: killing 10705 states (over memory cap)
KLEE: WARNING: killing 10385 states (over memory cap)
KLEE: WARNING: killing 10679 states (over memory cap)
KLEE: WARNING: killing 10820 states (over memory cap)
KLEE: WARNING: killing 10656 states (over memory cap)
KLEE: WARNING: killing 10948 states (over memory cap)
KLEE: WARNING: killing 10941 states (over memory cap)
KLEE: WARNING: killing 10929 states (over memory cap)
KLEE: WARNING: killing 10691 states (over memory cap)
KLEE: WARNING: killing 10905 states (over memory cap)
KLEE: WARNING: killing 10741 states (over memory cap)
KLEE: WARNING: killing 11037 states (over memory cap)
KLEE: WARNING: killing 10567 states (over memory cap)
KLEE: WARNING: killing 10480 states (over memory cap)
KLEE: WARNING: killing 10244 states (over memory cap)
KLEE: WARNING: killing 10228 states (over memory cap)
KLEE: WARNING: killing 10516 states (over memory cap)
KLEE: WARNING: killing 10430 states (over memory cap)
KLEE: WARNING: killing 10495 states (over memory cap)
KLEE: WARNING: killing 10480 states (over memory cap)
KLEE: WARNING: killing 10321 states (over memory cap)
KLEE: WARNING: killing 10609 states (over memory cap)
KLEE: WARNING: killing 10827 states (over memory cap)
KLEE: WARNING: killing 10814 states (over memory cap)
KLEE: WARNING: killing 10956 states (over memory cap)
KLEE: WARNING: killing 10794 states (over memory cap)
KLEE: WARNING: killing 10636 states (over memory cap)
KLEE: WARNING: killing 10706 states (over memory cap)
KLEE: WARNING: killing 10543 states (over memory cap)
KLEE: WARNING: killing 10679 states (over memory cap)
KLEE: WARNING: killing 11040 states (over memory cap)
KLEE: WARNING: killing 10807 states (over memory cap)
KLEE: WARNING: killing 10576 states (over memory cap)
KLEE: WARNING: killing 10717 states (over memory cap)
KLEE: WARNING: killing 10554 states (over memory cap)
KLEE: WARNING: killing 10837 states (over memory cap)
KLEE: WARNING: killing 10233 states (over memory cap)
KLEE: WARNING: killing 10592 states (over memory cap)
KLEE: WARNING: killing 10434 states (over memory cap)
KLEE: WARNING: killing 10863 states (over memory cap)
KLEE: WARNING: killing 10930 states (over memory cap)
KLEE: WARNING: killing 10473 states (over memory cap)
KLEE: WARNING: killing 10241 states (over memory cap)
KLEE: WARNING: killing 10379 states (over memory cap)
KLEE: WARNING: killing 10804 states (over memory cap)
KLEE: WARNING: killing 10649 states (over memory cap)
KLEE: WARNING: killing 10567 states (over memory cap)
KLEE: WARNING: killing 10994 states (over memory cap)
KLEE: WARNING: killing 10472 states (over memory cap)
KLEE: WARNING: killing 10467 states (over memory cap)
KLEE: WARNING: killing 11115 states (over memory cap)
KLEE: WARNING: killing 10815 states (over memory cap)
KLEE: WARNING: killing 10439 states (over memory cap)
KLEE: WARNING: killing 10422 states (over memory cap)
KLEE: WARNING: killing 10631 states (over memory cap)
KLEE: WARNING: killing 10837 states (over memory cap)
KLEE: WARNING: killing 10758 states (over memory cap)
KLEE: WARNING: killing 10312 states (over memory cap)
KLEE: WARNING: killing 10733 states (over memory cap)
KLEE: WARNING: killing 10873 states (over memory cap)
KLEE: WARNING: killing 10426 states (over memory cap)
KLEE: WARNING: killing 10053 states (over memory cap)
KLEE: WARNING: killing 10688 states (over memory cap)
KLEE: WARNING: killing 10457 states (over memory cap)
KLEE: WARNING: killing 10596 states (over memory cap)
KLEE: WARNING: killing 10804 states (over memory cap)
KLEE: WARNING: killing 10508 states (over memory cap)
KLEE: WARNING: killing 10567 states (over memory cap)
KLEE: WARNING: killing 10698 states (over memory cap)
KLEE: WARNING: killing 10479 states (over memory cap)
KLEE: WARNING: killing 10249 states (over memory cap)
KLEE: WARNING: killing 10378 states (over memory cap)
KLEE: WARNING: killing 10726 states (over memory cap)
KLEE: WARNING: killing 10572 states (over memory cap)
KLEE: WARNING: killing 11068 states (over memory cap)
KLEE: WARNING: killing 10626 states (over memory cap)
KLEE: WARNING: killing 10548 states (over memory cap)
KLEE: WARNING: killing 10680 states (over memory cap)
KLEE: WARNING: killing 10671 states (over memory cap)
KLEE: WARNING: killing 10873 states (over memory cap)
KLEE: WARNING: killing 10579 states (over memory cap)
KLEE: WARNING: killing 10569 states (over memory cap)
KLEE: WARNING: killing 10413 states (over memory cap)
KLEE: WARNING: killing 10260 states (over memory cap)
KLEE: WARNING: killing 10396 states (over memory cap)
KLEE: WARNING: killing 10807 states (over memory cap)
KLEE: WARNING: killing 11011 states (over memory cap)
KLEE: WARNING: killing 10649 states (over memory cap)
KLEE: WARNING: killing 10639 states (over memory cap)
KLEE: WARNING: killing 10839 states (over memory cap)
KLEE: WARNING: killing 10755 states (over memory cap)
KLEE: WARNING: killing 10394 states (over memory cap)
KLEE: WARNING: killing 10385 states (over memory cap)
KLEE: WARNING: killing 10799 states (over memory cap)
KLEE: WARNING: killing 10646 states (over memory cap)
KLEE: WARNING: killing 10778 states (over memory cap)
KLEE: WARNING: killing 10554 states (over memory cap)
KLEE: WARNING: killing 10407 states (over memory cap)
KLEE: WARNING: killing 10537 states (over memory cap)
KLEE: WARNING: killing 10596 states (over memory cap)
KLEE: WARNING: killing 10585 states (over memory cap)
KLEE: WARNING: killing 10434 states (over memory cap)
KLEE: WARNING: killing 10425 states (over memory cap)
KLEE: WARNING: killing 10345 states (over memory cap)
KLEE: WARNING: killing 10684 states (over memory cap)
KLEE: WARNING: killing 10463 states (over memory cap)
KLEE: WARNING: killing 10733 states (over memory cap)
KLEE: WARNING: killing 10517 states (over memory cap)
KLEE: WARNING: killing 10640 states (over memory cap)
KLEE: WARNING: killing 10630 states (over memory cap)
KLEE: WARNING: killing 10617 states (over memory cap)
KLEE: WARNING: killing 10610 states (over memory cap)
KLEE: WARNING: killing 10736 states (over memory cap)
KLEE: WARNING: killing 10590 states (over memory cap)
KLEE: WARNING: killing 11130 states (over memory cap)
KLEE: WARNING: killing 10775 states (over memory cap)
KLEE: WARNING: killing 10560 states (over memory cap)
KLEE: WARNING: killing 10686 states (over memory cap)
KLEE: WARNING: killing 10333 states (over memory cap)
KLEE: WARNING: killing 10665 states (over memory cap)
KLEE: WARNING: killing 11069 states (over memory cap)
KLEE: WARNING: killing 10510 states (over memory cap)
KLEE: WARNING: killing 10982 states (over memory cap)
KLEE: WARNING: killing 10833 states (over memory cap)
KLEE: WARNING: killing 10483 states (over memory cap)
KLEE: WARNING: killing 10747 states (over memory cap)
KLEE: WARNING: killing 10328 states (over memory cap)
KLEE: WARNING: killing 10316 states (over memory cap)
KLEE: WARNING: killing 10714 states (over memory cap)
KLEE: WARNING: killing 10296 states (over memory cap)
KLEE: WARNING: killing 10083 states (over memory cap)
