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--firewire--firewire-ohci.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.: 188 249 2073 13544
Removed infinite loop in dma_unmap_page
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_map_page
Removed infinite loop in dma_sync_single_for_device
Removed infinite loop in dma_sync_single_for_cpu
Removed infinite loop in dma_sync_single_range_for_cpu
Removed infinite loop in dma_sync_single_range_for_device
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.605599164963
Removed calls to 'dev_err' (function is undefined)
Removed calls to 'fw_card_initialize' (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 '__mutex_init' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'dev_notice' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Removed calls to 'pci_iounmap' (function is undefined)
Removed calls to 'pci_release_region' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'fw_core_remove_card' (function is undefined)
Removed calls to 'pci_restore_state' (function is undefined)
Defining function pci_set_power_state as symbolic
Defining function pci_enable_device as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to 'fw_schedule_bus_reset' (function is undefined)
Defining function dma_alloc_attrs as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'dump_stack' (function is undefined)
Defining function pci_save_state as symbolic
Defining function pci_choose_state as symbolic
Removed calls to 'vunmap' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Defining function cancel_work_sync as symbolic
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'fw_core_handle_bus_reset' (function is undefined)
Defining function pci_request_region as symbolic
Defining function pci_iomap as symbolic
Removed calls to 'tasklet_init' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function fw_card_add as symbolic
Defining function request_threaded_irq as symbolic
Removed calls to '__tasklet_schedule' (function is undefined)
Defining function __printk_ratelimit as symbolic
Defining function get_seconds as symbolic
Defining function sprintf as symbolic
Defining function queue_work_on as symbolic
Defining function pci_enable_msi_range as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'debug_dma_sync_single_for_device' (function is undefined)
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Defining function vmap as symbolic
Defining function alloc_pages_current as symbolic
Removed calls to 'fw_core_handle_request' (function is undefined)
Removed calls to 'fw_core_handle_response' (function is undefined)
Removed calls to 'debug_dma_sync_single_for_cpu' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function __memmove as symbolic
Defining function pci_bus_write_config_dword as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Removed calls to 'tasklet_kill' (function is undefined)
Removed calls to 'debug_dma_sync_single_range_for_cpu' (function is undefined)
Removed calls to 'debug_dma_sync_single_range_for_device' (function is undefined)
Defining function __get_free_pages as symbolic
Removed calls to 'fw_fill_response' (function is undefined)
Defining function __phys_addr as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Defining function ldv_suspend_late_3 as symbolic
Defining function ldv_resume_early_3 as symbolic
Defining function ldv_shutdown_3 as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function __pci_register_driver as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Defining function mutex_trylock as symbolic
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.657701015472
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 168 193 1159 7468
INFO: Starting verification
KLEE: WARNING ONCE: function "pci_probe" has inline asm
KLEE: WARNING ONCE: function "pci_remove" has inline asm
KLEE: WARNING ONCE: function "pci_resume" has inline asm
KLEE: WARNING ONCE: function "ohci_enable" has inline asm
KLEE: WARNING ONCE: function "ohci_start_iso" has inline asm
KLEE: WARNING ONCE: function "context_run" has inline asm
KLEE: WARNING ONCE: function "software_reset" has inline asm
KLEE: WARNING ONCE: function "read_phy_reg" has inline asm
KLEE: WARNING ONCE: function "ar_context_run" has inline asm
KLEE: WARNING ONCE: function "ar_context_link_page" has inline asm
KLEE: WARNING ONCE: function "write_phy_reg" has inline asm
KLEE: WARNING ONCE: function "bus_reset_work" has inline asm
KLEE: WARNING ONCE: function "irq_handler" has inline asm
KLEE: WARNING ONCE: function "tasklet_schedule" has inline asm
KLEE: WARNING ONCE: function "detect_dead_context" has inline asm
KLEE: WARNING ONCE: function "update_bus_time" has inline asm
KLEE: WARNING ONCE: function "get_cycle_time" has inline asm
KLEE: WARNING ONCE: function "context_stop" has inline asm
KLEE: WARNING ONCE: function "at_context_flush" has inline asm
KLEE: WARNING ONCE: function "ohci_set_config_rom" has inline asm
KLEE: WARNING ONCE: function "ohci_cancel_packet" has inline asm
KLEE: WARNING ONCE: function "ohci_enable_phys_dma" has inline asm
KLEE: WARNING ONCE: function "ohci_read_csr" has inline asm
KLEE: WARNING ONCE: function "ohci_write_csr" has inline asm
KLEE: WARNING ONCE: function "ohci_allocate_iso_context" has inline asm
KLEE: WARNING ONCE: function "ohci_set_iso_channels" has inline asm
KLEE: WARNING ONCE: function "ohci_flush_queue_iso" has inline asm
KLEE: WARNING ONCE: function "ohci_flush_iso_completions" has inline asm
KLEE: WARNING ONCE: function "ohci_stop_iso" has inline asm
KLEE: WARNING ONCE: function "dma_sync_single_range_for_cpu" has inline asm
KLEE: WARNING ONCE: function "dma_sync_single_range_for_device" has inline asm
KLEE: WARNING ONCE: function "context_append" has inline asm
KLEE: WARNING ONCE: function "at_context_transmit" has inline asm
KLEE: WARNING ONCE: function "main" 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_8621608e-4e7c-48a2-9ab7-ebf6e8d3dc6c/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-12P11d/linux-4.2-rc1.tar.xz-32_7a-drivers--firewire--firewire-ohci.ko-entry_point_true-unreach-call.cil.out.c:7789: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-12P11d/linux-4.2-rc1.tar.xz-32_7a-drivers--firewire--firewire-ohci.ko-entry_point_true-unreach-call.cil.out.c:7676: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-12P11d/linux-4.2-rc1.tar.xz-32_7a-drivers--firewire--firewire-ohci.ko-entry_point_true-unreach-call.cil.out.c:7241: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-12P11d/linux-4.2-rc1.tar.xz-32_7a-drivers--firewire--firewire-ohci.ko-entry_point_true-unreach-call.cil.out.c:7847: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-12P11d/linux-4.2-rc1.tar.xz-32_7a-drivers--firewire--firewire-ohci.ko-entry_point_true-unreach-call.cil.out.c:8282: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-12P11d/linux-4.2-rc1.tar.xz-32_7a-drivers--firewire--firewire-ohci.ko-entry_point_true-unreach-call.cil.out.c:4872: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-12P11d/linux-4.2-rc1.tar.xz-32_7a-drivers--firewire--firewire-ohci.ko-entry_point_true-unreach-call.cil.out.c:3732: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-12P11d/linux-4.2-rc1.tar.xz-32_7a-drivers--firewire--firewire-ohci.ko-entry_point_true-unreach-call.cil.out.c:6125: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-12P11d/linux-4.2-rc1.tar.xz-32_7a-drivers--firewire--firewire-ohci.ko-entry_point_true-unreach-call.cil.out.c:3732: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-12P11d/linux-4.2-rc1.tar.xz-32_7a-drivers--firewire--firewire-ohci.ko-entry_point_true-unreach-call.cil.out.c:4844: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-12P11d/linux-4.2-rc1.tar.xz-32_7a-drivers--firewire--firewire-ohci.ko-entry_point_true-unreach-call.cil.out.c:8308: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-12P11d/linux-4.2-rc1.tar.xz-32_7a-drivers--firewire--firewire-ohci.ko-entry_point_true-unreach-call.cil.out.c:7203: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-12P11d/linux-4.2-rc1.tar.xz-32_7a-drivers--firewire--firewire-ohci.ko-entry_point_true-unreach-call.cil.out.c:7101: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 14376 states (over memory cap)
KLEE: WARNING: killing 13075 states (over memory cap)
KLEE: WARNING: killing 12849 states (over memory cap)
KLEE: WARNING: killing 13326 states (over memory cap)
KLEE: WARNING: killing 13447 states (over memory cap)
KLEE: WARNING: killing 13142 states (over memory cap)
KLEE: WARNING: killing 13708 states (over memory cap)
KLEE: WARNING: killing 14715 states (over memory cap)
KLEE: WARNING: killing 14407 states (over memory cap)
KLEE: WARNING: killing 13932 states (over memory cap)
KLEE: WARNING: killing 14671 states (over memory cap)
KLEE: WARNING: killing 14547 states (over memory cap)
KLEE: WARNING: killing 14771 states (over memory cap)
KLEE: WARNING: killing 14902 states (over memory cap)
KLEE: WARNING: killing 14870 states (over memory cap)
KLEE: WARNING: killing 14663 states (over memory cap)
KLEE: WARNING: killing 14195 states (over memory cap)
KLEE: WARNING: killing 14583 states (over memory cap)
KLEE: WARNING: killing 14120 states (over memory cap)
KLEE: WARNING: killing 14337 states (over memory cap)
KLEE: WARNING: killing 14886 states (over memory cap)
KLEE: WARNING: killing 14595 states (over memory cap)
KLEE: WARNING: killing 14477 states (over memory cap)
KLEE: WARNING: killing 14522 states (over memory cap)
KLEE: WARNING: killing 14065 states (over memory cap)
KLEE: WARNING: killing 14284 states (over memory cap)
KLEE: WARNING: killing 14745 states (over memory cap)
KLEE: WARNING: killing 14462 states (over memory cap)
KLEE: WARNING: killing 14345 states (over memory cap)
KLEE: WARNING: killing 14319 states (over memory cap)
KLEE: WARNING: killing 14445 states (over memory cap)
KLEE: WARNING: killing 14579 states (over memory cap)
KLEE: WARNING: killing 14876 states (over memory cap)
KLEE: WARNING: killing 14689 states (over memory cap)
KLEE: WARNING: killing 13997 states (over memory cap)
KLEE: WARNING: killing 14452 states (over memory cap)
KLEE: WARNING: killing 14094 states (over memory cap)
KLEE: WARNING: killing 14469 states (over memory cap)
KLEE: WARNING: killing 14194 states (over memory cap)
KLEE: WARNING: killing 14250 states (over memory cap)
KLEE: WARNING: killing 14468 states (over memory cap)
KLEE: WARNING: killing 14111 states (over memory cap)
KLEE: WARNING: killing 14561 states (over memory cap)
KLEE: WARNING: killing 14287 states (over memory cap)
KLEE: WARNING: killing 14739 states (over memory cap)
KLEE: WARNING: killing 14475 states (over memory cap)
KLEE: WARNING: killing 14451 states (over memory cap)
KLEE: WARNING: killing 14180 states (over memory cap)
KLEE: WARNING: killing 14396 states (over memory cap)
KLEE: WARNING: killing 14118 states (over memory cap)
KLEE: WARNING: killing 14009 states (over memory cap)
KLEE: WARNING: killing 14457 states (over memory cap)
KLEE: WARNING: killing 14666 states (over memory cap)
KLEE: WARNING: killing 14403 states (over memory cap)
KLEE: WARNING: killing 13906 states (over memory cap)
KLEE: WARNING: killing 7812 states (over memory cap)
KLEE: WARNING: killing 14027 states (over memory cap)
KLEE: WARNING: killing 14463 states (over memory cap)
KLEE: WARNING: killing 14362 states (over memory cap)
KLEE: WARNING: killing 13948 states (over memory cap)
KLEE: WARNING: killing 14313 states (over memory cap)
KLEE: WARNING: killing 7808 states (over memory cap)
KLEE: WARNING: killing 13262 states (over memory cap)
KLEE: WARNING: killing 14391 states (over memory cap)
KLEE: WARNING: killing 7772 states (over memory cap)
KLEE: WARNING: killing 13586 states (over memory cap)
KLEE: WARNING: killing 7677 states (over memory cap)
KLEE: WARNING: killing 14171 states (over memory cap)
KLEE: WARNING: killing 8038 states (over memory cap)
KLEE: WARNING: killing 14141 states (over memory cap)
KLEE: WARNING: killing 7715 states (over memory cap)
KLEE: WARNING: killing 13411 states (over memory cap)
KLEE: WARNING: killing 14231 states (over memory cap)
KLEE: WARNING: killing 7606 states (over memory cap)
KLEE: WARNING: killing 13733 states (over memory cap)
KLEE: WARNING: killing 13783 states (over memory cap)
KLEE: WARNING: killing 7647 states (over memory cap)
KLEE: WARNING: killing 13362 states (over memory cap)
KLEE: WARNING: killing 7774 states (over memory cap)
KLEE: WARNING: killing 13787 states (over memory cap)
KLEE: WARNING: killing 7528 states (over memory cap)
KLEE: WARNING: killing 13827 states (over memory cap)
KLEE: WARNING: killing 7586 states (over memory cap)
KLEE: WARNING: killing 13872 states (over memory cap)
KLEE: WARNING: killing 7566 states (over memory cap)
KLEE: WARNING: killing 14139 states (over memory cap)
KLEE: WARNING: killing 7846 states (over memory cap)
KLEE: WARNING: killing 13952 states (over memory cap)
KLEE: WARNING: killing 7904 states (over memory cap)
KLEE: WARNING: killing 13391 states (over memory cap)
KLEE: WARNING: killing 7729 states (over memory cap)
KLEE: WARNING: killing 13576 states (over memory cap)
KLEE: WARNING: killing 7855 states (over memory cap)
KLEE: WARNING: killing 7405 states (over memory cap)
KLEE: WARNING: killing 13903 states (over memory cap)
KLEE: WARNING: killing 7535 states (over memory cap)
KLEE: WARNING: killing 7531 states (over memory cap)
KLEE: WARNING: killing 7374 states (over memory cap)
KLEE: WARNING: killing 13694 states (over memory cap)
KLEE: WARNING: killing 7725 states (over memory cap)
KLEE: WARNING: killing 14034 states (over memory cap)
KLEE: WARNING: killing 7632 states (over memory cap)
KLEE: WARNING: killing 13780 states (over memory cap)
KLEE: WARNING: killing 7464 states (over memory cap)
KLEE: WARNING: killing 13661 states (over memory cap)
KLEE: WARNING: killing 7520 states (over memory cap)
KLEE: WARNING: killing 7511 states (over memory cap)
KLEE: WARNING: killing 13254 states (over memory cap)
KLEE: WARNING: killing 7929 states (over memory cap)
KLEE: WARNING: killing 13798 states (over memory cap)
KLEE: WARNING: killing 7547 states (over memory cap)
KLEE: WARNING: killing 13621 states (over memory cap)
KLEE: WARNING: killing 8034 states (over memory cap)
KLEE: WARNING: killing 7304 states (over memory cap)
KLEE: WARNING: killing 13649 states (over memory cap)
KLEE: WARNING: killing 7644 states (over memory cap)
KLEE: WARNING: killing 7419 states (over memory cap)
KLEE: WARNING: killing 7270 states (over memory cap)
KLEE: WARNING: killing 13446 states (over memory cap)
KLEE: WARNING: killing 7398 states (over memory cap)
KLEE: WARNING: killing 7247 states (over memory cap)
KLEE: WARNING: killing 7600 states (over memory cap)
KLEE: WARNING: killing 7310 states (over memory cap)
KLEE: WARNING: killing 13531 states (over memory cap)
KLEE: WARNING: killing 7786 states (over memory cap)
KLEE: WARNING: killing 7284 states (over memory cap)
KLEE: WARNING: killing 7421 states (over memory cap)
KLEE: WARNING: killing 7273 states (over memory cap)
KLEE: WARNING: killing 13099 states (over memory cap)
KLEE: WARNING: killing 7746 states (over memory cap)
KLEE: WARNING: killing 7102 states (over memory cap)
KLEE: WARNING: killing 7310 states (over memory cap)
KLEE: WARNING: killing 7305 states (over memory cap)
KLEE: WARNING: killing 13605 states (over memory cap)
KLEE: WARNING: killing 7710 states (over memory cap)
KLEE: WARNING: killing 13500 states (over memory cap)
KLEE: WARNING: killing 7688 states (over memory cap)
KLEE: WARNING: killing 13387 states (over memory cap)
KLEE: WARNING: killing 7667 states (over memory cap)
KLEE: WARNING: killing 7168 states (over memory cap)
KLEE: WARNING: killing 13411 states (over memory cap)
KLEE: WARNING: killing 7919 states (over memory cap)
KLEE: WARNING: killing 7214 states (over memory cap)
KLEE: WARNING: killing 7137 states (over memory cap)
KLEE: WARNING: killing 7062 states (over memory cap)
KLEE: WARNING: killing 7193 states (over memory cap)
KLEE: WARNING: killing 7398 states (over memory cap)
KLEE: WARNING: killing 7112 states (over memory cap)
KLEE: WARNING: killing 7036 states (over memory cap)
KLEE: WARNING: killing 7728 states (over memory cap)
KLEE: WARNING: killing 7168 states (over memory cap)
KLEE: WARNING: killing 7300 states (over memory cap)
KLEE: WARNING: killing 7157 states (over memory cap)
KLEE: WARNING: killing 7152 states (over memory cap)
KLEE: WARNING: killing 7218 states (over memory cap)
KLEE: WARNING: killing 7143 states (over memory cap)
