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--block--rsxx--rsxx.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.: 305 412 2752 17721
Removed infinite loop in creg_cmd_done_cb
Removed infinite loop in dma_unmap_page
Removed infinite loop in dma_map_page
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.709797143936
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Defining function ioread32 as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'dev_crit' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'dev_warn' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to 'kmem_cache_free' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to 'complete' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function wait_for_completion_timeout as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'iowrite32' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function mutex_trylock as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function kmem_cache_alloc as symbolic
Removed calls to 'iowrite32be' (function is undefined)
Defining function mod_timer as symbolic
Defining function _copy_from_user as symbolic
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Removed calls to '_dev_info' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to '__raw_spin_lock_init' (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 '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'debugfs_remove' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Removed calls to 'pci_iounmap' (function is undefined)
Removed calls to 'pci_release_regions' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'ida_remove' (function is undefined)
Removed calls to 'debugfs_remove_recursive' (function is undefined)
Removed calls to 'del_gendisk' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'put_disk' (function is undefined)
Removed calls to 'blk_cleanup_queue' (function is undefined)
Removed calls to 'unregister_blkdev' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Defining function cancel_work_sync as symbolic
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function ioread32be as symbolic
Defining function ida_pre_get as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_set_dma_max_seg_size as symbolic
Defining function pci_request_regions as symbolic
Defining function pci_iomap as symbolic
Removed calls to '__mutex_init' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Removed calls to 'blk_queue_dma_alignment' (function is undefined)
Removed calls to 'blk_queue_logical_block_size' (function is undefined)
Removed calls to 'blk_queue_make_request' (function is undefined)
Removed calls to 'blk_queue_bounce_limit' (function is undefined)
Removed calls to 'blk_queue_max_hw_sectors' (function is undefined)
Removed calls to 'blk_queue_physical_block_size' (function is undefined)
Removed calls to 'blk_queue_max_discard_sectors' (function is undefined)
Removed calls to 'add_disk' (function is undefined)
Defining function debugfs_create_dir as symbolic
Defining function debugfs_create_file as symbolic
Defining function register_blkdev as symbolic
Defining function blk_alloc_queue as symbolic
Defining function alloc_disk as symbolic
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'generic_start_io_acct' (function is undefined)
Removed calls to 'bio_endio' (function is undefined)
Defining function snprintf as symbolic
Defining function pci_bus_read_config_byte as symbolic
Removed calls to 'generic_end_io_acct' (function is undefined)
Defining function queue_work_on as symbolic
Removed calls to 'dev_emerg' (function is undefined)
Removed calls to 'dev_alert' (function is undefined)
Removed calls to 'dev_notice' (function is undefined)
Defining function vmalloc as symbolic
Removed calls to 'debug_dma_map_page' (function is undefined)
Defining function dma_alloc_attrs as symbolic
Defining function crc32_le as symbolic
Defining function request_threaded_irq as symbolic
Defining function pci_enable_msi_range as symbolic
Defining function dma_set_mask as symbolic
Defining function ida_get_new_above as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Defining function ldv_resume_9 as symbolic
Defining function ldv_suspend_late_9 as symbolic
Defining function ldv_resume_early_9 as symbolic
Defining function ldv_open_13 as symbolic
Defining function ldv_release_13 as symbolic
Defining function __pci_register_driver as symbolic
Defining function kmem_cache_create 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.695524930954
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 302 354 1660 9520
INFO: Starting verification
KLEE: WARNING ONCE: function "creg_cmd_done_cb" has inline asm
KLEE: WARNING ONCE: function "rsxx_dma_cancel" has inline asm
KLEE: WARNING ONCE: function "pci_unmap_page" has inline asm
KLEE: WARNING ONCE: function "rsxx_setup_dev" has inline asm
KLEE: WARNING ONCE: function "rsxx_card_state_to_str" has inline asm
KLEE: WARNING ONCE: function "rsxx_schedule_issue" has inline asm
KLEE: WARNING ONCE: function "rsxx_schedule_done" has inline asm
KLEE: WARNING ONCE: function "rsxx_dma_configure" has inline asm
KLEE: WARNING ONCE: function "rsxx_error_detected" has inline asm
KLEE: WARNING ONCE: function "rsxx_eeh_save_issued_dmas" has inline asm
KLEE: WARNING ONCE: function "rsxx_reg_access" has inline asm
KLEE: WARNING ONCE: function "rsxx_dma_queue_bio" 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_3a8d9d04-14cd-4acd-871b-ad875f963ce2/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12490 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 13605 states (over memory cap)
KLEE: WARNING: killing 13305 states (over memory cap)
KLEE: WARNING: killing 13089 states (over memory cap)
KLEE: WARNING: killing 13058 states (over memory cap)
KLEE: WARNING: killing 12499 states (over memory cap)
KLEE: WARNING: killing 12995 states (over memory cap)
KLEE: WARNING: killing 12794 states (over memory cap)
KLEE: WARNING: killing 13111 states (over memory cap)
KLEE: WARNING: killing 12736 states (over memory cap)
KLEE: WARNING: killing 13052 states (over memory cap)
KLEE: WARNING: killing 12764 states (over memory cap)
KLEE: WARNING: killing 12828 states (over memory cap)
KLEE: WARNING: killing 13317 states (over memory cap)
KLEE: WARNING: killing 13725 states (over memory cap)
KLEE: WARNING: killing 14473 states (over memory cap)
KLEE: WARNING: killing 13680 states (over memory cap)
KLEE: WARNING: killing 13824 states (over memory cap)
KLEE: WARNING: killing 14663 states (over memory cap)
KLEE: WARNING: killing 14219 states (over memory cap)
KLEE: WARNING: killing 14883 states (over memory cap)
KLEE: WARNING: killing 15032 states (over memory cap)
KLEE: WARNING: killing 14251 states (over memory cap)
KLEE: WARNING: killing 14145 states (over memory cap)
KLEE: WARNING: killing 13953 states (over memory cap)
KLEE: WARNING: killing 13594 states (over memory cap)
KLEE: WARNING: killing 13744 states (over memory cap)
KLEE: WARNING: killing 13377 states (over memory cap)
KLEE: WARNING: killing 14039 states (over memory cap)
KLEE: WARNING: killing 14094 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-eLJSFl/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rsxx--rsxx.ko-entry_point_true-unreach-call.cil.out.c:5547: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-eLJSFl/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rsxx--rsxx.ko-entry_point_true-unreach-call.cil.out.c:6102: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-eLJSFl/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rsxx--rsxx.ko-entry_point_true-unreach-call.cil.out.c:9716: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14410 states (over memory cap)
KLEE: WARNING: killing 14306 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-eLJSFl/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rsxx--rsxx.ko-entry_point_true-unreach-call.cil.out.c:6194: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13608 states (over memory cap)
KLEE: WARNING: killing 13338 states (over memory cap)
KLEE: WARNING: killing 13902 states (over memory cap)
KLEE: WARNING: killing 13294 states (over memory cap)
KLEE: WARNING: killing 13027 states (over memory cap)
KLEE: WARNING: killing 14171 states (over memory cap)
KLEE: WARNING: killing 13401 states (over memory cap)
KLEE: WARNING: killing 14300 states (over memory cap)
KLEE: WARNING: killing 13778 states (over memory cap)
KLEE: WARNING: killing 14589 states (over memory cap)
KLEE: WARNING: killing 14079 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-eLJSFl/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rsxx--rsxx.ko-entry_point_true-unreach-call.cil.out.c:6011: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13557 states (over memory cap)
KLEE: WARNING: killing 13710 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-eLJSFl/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rsxx--rsxx.ko-entry_point_true-unreach-call.cil.out.c:5507: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13935 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-eLJSFl/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rsxx--rsxx.ko-entry_point_true-unreach-call.cil.out.c:6166: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14165 states (over memory cap)
KLEE: WARNING: killing 13654 states (over memory cap)
KLEE: WARNING: killing 13878 states (over memory cap)
KLEE: WARNING: killing 13292 states (over memory cap)
KLEE: WARNING: killing 14095 states (over memory cap)
KLEE: WARNING: killing 13826 states (over memory cap)
KLEE: WARNING: killing 14057 states (over memory cap)
KLEE: WARNING: killing 13623 states (over memory cap)
KLEE: WARNING: killing 14100 states (over memory cap)
KLEE: WARNING: killing 13593 states (over memory cap)
KLEE: WARNING: killing 13734 states (over memory cap)
KLEE: WARNING: killing 14205 states (over memory cap)
KLEE: WARNING: killing 14348 states (over memory cap)
KLEE: WARNING: killing 14013 states (over memory cap)
KLEE: WARNING: killing 13992 states (over memory cap)
KLEE: WARNING: killing 13981 states (over memory cap)
KLEE: WARNING: killing 14365 states (over memory cap)
KLEE: WARNING: killing 13786 states (over memory cap)
KLEE: WARNING: killing 13525 states (over memory cap)
KLEE: WARNING: killing 13429 states (over memory cap)
KLEE: WARNING: killing 13489 states (over memory cap)
KLEE: WARNING: killing 14437 states (over memory cap)
KLEE: WARNING: killing 13779 states (over memory cap)
KLEE: WARNING: killing 14081 states (over memory cap)
KLEE: WARNING: killing 13422 states (over memory cap)
KLEE: WARNING: killing 14370 states (over memory cap)
KLEE: WARNING: killing 13546 states (over memory cap)
KLEE: WARNING: killing 13846 states (over memory cap)
KLEE: WARNING: killing 14235 states (over memory cap)
KLEE: WARNING: killing 14060 states (over memory cap)
KLEE: WARNING: killing 13886 states (over memory cap)
KLEE: WARNING: killing 13715 states (over memory cap)
KLEE: WARNING: killing 13537 states (over memory cap)
KLEE: WARNING: killing 13682 states (over memory cap)
KLEE: WARNING: killing 13907 states (over memory cap)
KLEE: WARNING: killing 14361 states (over memory cap)
KLEE: WARNING: killing 14029 states (over memory cap)
KLEE: WARNING: killing 13704 states (over memory cap)
KLEE: WARNING: killing 14159 states (over memory cap)
KLEE: WARNING: killing 13910 states (over memory cap)
KLEE: WARNING: killing 13895 states (over memory cap)
KLEE: WARNING: killing 13958 states (over memory cap)
KLEE: WARNING: killing 13314 states (over memory cap)
KLEE: WARNING: killing 13296 states (over memory cap)
KLEE: WARNING: killing 13903 states (over memory cap)
KLEE: WARNING: killing 14202 states (over memory cap)
KLEE: WARNING: killing 13878 states (over memory cap)
KLEE: WARNING: killing 13932 states (over memory cap)
KLEE: WARNING: killing 13766 states (over memory cap)
KLEE: WARNING: killing 14146 states (over memory cap)
KLEE: WARNING: killing 13897 states (over memory cap)
KLEE: WARNING: killing 14432 states (over memory cap)
KLEE: WARNING: killing 13400 states (over memory cap)
KLEE: WARNING: killing 13615 states (over memory cap)
KLEE: WARNING: killing 13835 states (over memory cap)
KLEE: WARNING: killing 13741 states (over memory cap)
KLEE: WARNING: killing 14196 states (over memory cap)
KLEE: WARNING: killing 13945 states (over memory cap)
KLEE: WARNING: killing 13321 states (over memory cap)
KLEE: WARNING: killing 14002 states (over memory cap)
KLEE: WARNING: killing 14070 states (over memory cap)
KLEE: WARNING: killing 13819 states (over memory cap)
KLEE: WARNING: killing 13422 states (over memory cap)
KLEE: WARNING: killing 13791 states (over memory cap)
KLEE: WARNING: killing 14243 states (over memory cap)
KLEE: WARNING: killing 13995 states (over memory cap)
KLEE: WARNING: killing 13906 states (over memory cap)
KLEE: WARNING: killing 13965 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-eLJSFl/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rsxx--rsxx.ko-entry_point_true-unreach-call.cil.out.c:8091: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13725 states (over memory cap)
KLEE: WARNING: killing 13403 states (over memory cap)
KLEE: WARNING: killing 13998 states (over memory cap)
KLEE: WARNING: killing 13526 states (over memory cap)
KLEE: WARNING: killing 13519 states (over memory cap)
KLEE: WARNING: killing 13650 states (over memory cap)
KLEE: WARNING: killing 13862 states (over memory cap)
KLEE: WARNING: killing 14305 states (over memory cap)
KLEE: WARNING: killing 13758 states (over memory cap)
KLEE: WARNING: killing 13892 states (over memory cap)
KLEE: WARNING: killing 14179 states (over memory cap)
KLEE: WARNING: killing 14017 states (over memory cap)
KLEE: WARNING: killing 14238 states (over memory cap)
KLEE: WARNING: killing 13923 states (over memory cap)
KLEE: WARNING: killing 13307 states (over memory cap)
KLEE: WARNING: killing 14201 states (over memory cap)
KLEE: WARNING: killing 14111 states (over memory cap)
KLEE: WARNING: killing 13187 states (over memory cap)
KLEE: WARNING: killing 13397 states (over memory cap)
KLEE: WARNING: killing 13984 states (over memory cap)
KLEE: WARNING: killing 13374 states (over memory cap)
KLEE: WARNING: killing 13358 states (over memory cap)
