bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--scsi--aacraid--aacraid.ko_false-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.: 322 825 6024 39442
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_linux_kernel_module_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 1.22560715675
Removed calls to 'msleep' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'ldv_free_irq' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Defining function printk as symbolic
Removed calls to '__const_udelay' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Defining function get_seconds as symbolic
Defining function ldv_request_irq as symbolic
Defining function request_threaded_irq as symbolic
Defining function pci_enable_msi_range as symbolic
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function dma_get_required_mask as symbolic
Removed calls to '__ldv_linux_kernel_locking_spinlock_spin_lock' (function is undefined)
Removed calls to 'up' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function down_interruptible as symbolic
Defining function down_trylock as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Defining function hex_to_bin as symbolic
Defining function external_allocated_data as symbolic
Defining function snprintf as symbolic
Removed calls to 'pci_disable_link_state' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to 'scsi_scan_host' (function is undefined)
Removed calls to 'scsi_host_put' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'scsi_remove_host' (function is undefined)
Removed calls to 'scsi_block_requests' (function is undefined)
Defining function kthread_stop as symbolic
Removed calls to '__unregister_chrdev' (function is undefined)
Defining function pci_enable_device as symbolic
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'do_gettimeofday' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function pci_set_dma_max_seg_size as symbolic
Removed calls to 'ldv_pre_probe' (function is undefined)
Defining function scsi_bios_ptable as symbolic
Defining function scsi_change_queue_depth as symbolic
Defining function capable as symbolic
Removed calls to 'might_fault' (function is undefined)
Defining function compat_alloc_user_space as symbolic
Defining function clear_user as symbolic
Defining function copy_in_user as symbolic
Defining function _copy_to_user as symbolic
Removed calls to 'debug_dma_map_page' (function is undefined)
Defining function __phys_addr as symbolic
Defining function _copy_from_user as symbolic
Defining function simple_strtol as symbolic
Defining function strlcpy as symbolic
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'scsi_unblock_requests' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Defining function __ldv_linux_kernel_locking_spinlock_spin_trylock as symbolic
Defining function noop_llseek as symbolic
Removed calls to 'scsi_cmd_get_serial' (function is undefined)
Defining function sg_copy_to_buffer as symbolic
Defining function sg_copy_from_buffer as symbolic
Removed calls to 'blk_queue_rq_timeout' (function is undefined)
Defining function scsi_add_host_with_dma as symbolic
Removed calls to 'scsi_dma_unmap' (function is undefined)
Defining function scsi_dma_map as symbolic
Defining function sg_next as symbolic
Defining function default_wake_function as symbolic
Removed calls to 'scsi_device_put' (function is undefined)
Removed calls to 'scsi_remove_device' (function is undefined)
Removed calls to 'sdev_prefix_printk' (function is undefined)
Removed calls to 'scsi_rescan_device' (function is undefined)
Defining function schedule_timeout as symbolic
Defining function kthread_should_stop as symbolic
Defining function scsi_device_lookup as symbolic
Defining function scsi_device_set_state as symbolic
Defining function scsi_add_device as symbolic
Defining function scsi_host_alloc as symbolic
Defining function dma_supported as symbolic
Defining function dma_set_mask as symbolic
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function __register_chrdev as symbolic
Defining function __pci_register_driver as symbolic
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  memcmp
  strlen
  __memcpy
  __memset
  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: 1.24478816986
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 524 700 3807 23633
INFO: Starting verification
KLEE: WARNING ONCE: function "aac_sa_init" has inline asm
KLEE: WARNING ONCE: function "aac_src_init" has inline asm
KLEE: WARNING ONCE: function "aac_srcv_init" has inline asm
KLEE: WARNING ONCE: function "src_sync_cmd" has inline asm
KLEE: WARNING ONCE: function "aac_src_disable_interrupt" has inline asm
KLEE: WARNING ONCE: function "aac_src_restart_adapter" has inline asm
KLEE: WARNING ONCE: function "aac_src_notify_adapter" has inline asm
KLEE: WARNING ONCE: function "aac_src_check_health" has inline asm
KLEE: WARNING ONCE: function "aac_src_enable_interrupt_message" has inline asm
KLEE: WARNING ONCE: function "aac_src_intr_message" has inline asm
KLEE: WARNING ONCE: function "aac_src_deliver_message" has inline asm
KLEE: WARNING ONCE: function "aac_aif_callback" has inline asm
KLEE: WARNING ONCE: function "aac_fib_send" has inline asm
KLEE: WARNING ONCE: function "aac_fib_complete" has inline asm
KLEE: WARNING ONCE: function "_aac_rx_init" has inline asm
KLEE: WARNING ONCE: function "rx_sync_cmd" has inline asm
KLEE: WARNING ONCE: function "aac_rx_disable_interrupt" has inline asm
KLEE: WARNING ONCE: function "aac_rx_restart_adapter" has inline asm
KLEE: WARNING ONCE: function "aac_rx_check_health" has inline asm
KLEE: WARNING ONCE: function "aac_rx_notify_adapter" has inline asm
KLEE: WARNING ONCE: function "pci_free_consistent" has inline asm
KLEE: WARNING ONCE: function "aac_rx_enable_interrupt_producer" has inline asm
KLEE: WARNING ONCE: function "aac_rx_intr_producer" has inline asm
KLEE: WARNING ONCE: function "aac_rx_enable_interrupt_message" has inline asm
KLEE: WARNING ONCE: function "aac_rx_intr_message" has inline asm
KLEE: WARNING ONCE: function "aac_rx_deliver_message" has inline asm
KLEE: WARNING ONCE: function "aac_fib_adapter_complete" has inline asm
KLEE: WARNING ONCE: function "aac_sa_disable_interrupt" has inline asm
KLEE: WARNING ONCE: function "aac_sa_enable_interrupt" has inline asm
KLEE: WARNING ONCE: function "aac_sa_notify_adapter" has inline asm
KLEE: WARNING ONCE: function "sa_sync_cmd" has inline asm
KLEE: WARNING ONCE: function "aac_sa_check_health" has inline asm
KLEE: WARNING ONCE: function "aac_sa_intr" has inline asm
KLEE: WARNING ONCE: function "aac_command_thread" has inline asm
KLEE: WARNING ONCE: function "pci_map_single" has inline asm
KLEE: WARNING ONCE: function "aac_check_health" has inline asm
KLEE: WARNING ONCE: function "_aac_reset_adapter" has inline asm
KLEE: WARNING ONCE: function "get_container_serial_callback" has inline asm
KLEE: WARNING ONCE: function "get_container_name_callback" has inline asm
KLEE: WARNING ONCE: function "aac_start_stop_callback" has inline asm
KLEE: WARNING ONCE: function "aac_scsi_64" has inline asm
KLEE: WARNING ONCE: function "aac_scsi_32" has inline asm
KLEE: WARNING ONCE: function "aac_read_raw_io" has inline asm
KLEE: WARNING ONCE: function "aac_write_raw_io" has inline asm
KLEE: WARNING ONCE: function "aac_read_block64" has inline asm
KLEE: WARNING ONCE: function "aac_write_block64" has inline asm
KLEE: WARNING ONCE: function "aac_read_block" has inline asm
KLEE: WARNING ONCE: function "aac_write_block" has inline asm
KLEE: WARNING ONCE: function "io_callback" has inline asm
KLEE: WARNING ONCE: function "aac_build_sgraw2" has inline asm
KLEE: WARNING ONCE: function "aac_srb_callback" has inline asm
KLEE: WARNING ONCE: function "aac_consumer_free" 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_911bd0d1-46e7-48be-9d33-0936c0f52933/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GDpQcJ/linux-4.0-rc1---drivers--scsi--aacraid--aacraid.ko_false-unreach-call.cil.c:8572: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 10680 bytes on read, may be slow and/or crash: MO84[10680] allocated at global:
KLEE: ERROR: /tmp/symbiotic-GDpQcJ/linux-4.0-rc1---drivers--scsi--aacraid--aacraid.ko_false-unreach-call.cil.c:8253: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GDpQcJ/linux-4.0-rc1---drivers--scsi--aacraid--aacraid.ko_false-unreach-call.cil.c:8253: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GDpQcJ/linux-4.0-rc1---drivers--scsi--aacraid--aacraid.ko_false-unreach-call.cil.c:8255: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GDpQcJ/linux-4.0-rc1---drivers--scsi--aacraid--aacraid.ko_false-unreach-call.cil.c:8255: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GDpQcJ/linux-4.0-rc1---drivers--scsi--aacraid--aacraid.ko_false-unreach-call.cil.c:9585: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
