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-43_2a-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.: 97 169 2119 12614
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 2.95771598816
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)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function vfio_device_get_from_dev as symbolic
Defining function vfio_device_data as symbolic
Defining function eventfd_signal as symbolic
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 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)
Removed calls to 'ldv_check_final_state' (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 ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strlen
  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.30970001221
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 202 179 1182 7347
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_6698ef08-d254-4ed3-a57f-7c71b9a744ca/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_6698ef08-d254-4ed3-a57f-7c71b9a744ca/symbiotic/lib/kernel/kfree.c:5: memory error: invalid pointer: free
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_6698ef08-d254-4ed3-a57f-7c71b9a744ca/symbiotic/lib/kernel/kfree.c:5: free of global
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_6698ef08-d254-4ed3-a57f-7c71b9a744ca/symbiotic/lib/kernel/kfree.c:5: free of alloca
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139384: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139384: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139385: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139385: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_6698ef08-d254-4ed3-a57f-7c71b9a744ca/symbiotic/lib/kernel/kfree.c:5: memory error: invalid pointer: free
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_6698ef08-d254-4ed3-a57f-7c71b9a744ca/symbiotic/lib/kernel/kfree.c:5: free of global
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_6698ef08-d254-4ed3-a57f-7c71b9a744ca/symbiotic/lib/kernel/kfree.c:5: free of alloca
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139384: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139385: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139384: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139385: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139384: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139385: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139374: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139375: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139394: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139395: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139394: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139395: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139394: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139395: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139394: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139395: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139394: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139374: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139374: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139395: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139394: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139395: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139375: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139375: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139394: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_yt_1Y/linux-4.2-rc1.tar.xz-43_2a-drivers--vfio--pci--vfio-pci.ko-entry_point_true-unreach-call.cil.out.c:139394: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
