bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--block--cpqarray.ko-main.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.: 155 163 1232 7934
Removed infinite loop in do_ida_request
Removed infinite loop in arch_local_save_flags
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in sg_page
Removed infinite loop in dma_map_page
Removed infinite loop in dma_unmap_page
INFO: Compilation, preparation and instrumentation time: 0.397430181503
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'del_gendisk' (function is undefined)
Removed calls to 'blk_queue_logical_block_size' (function is undefined)
Removed calls to 'add_disk' (function is undefined)
Defining function single_release as symbolic
Defining function seq_read as symbolic
Defining function seq_lseek as symbolic
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'blk_queue_bounce_limit' (function is undefined)
Removed calls to 'blk_queue_max_segments' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'put_disk' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'unregister_blkdev' (function is undefined)
Defining function printk as symbolic
Defining function __pci_register_driver as symbolic
Defining function __request_region as symbolic
Defining function sprintf as symbolic
Defining function register_blkdev as symbolic
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Removed calls to '__blk_end_request_all' (function is undefined)
Defining function alloc_disk as symbolic
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Removed calls to 'blk_start_request' (function is undefined)
Removed calls to 'sg_init_table' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Defining function blk_init_queue as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Defining function dev_set_drvdata as symbolic
Defining function proc_mkdir as symbolic
Defining function proc_create_data as symbolic
Removed calls to '__const_udelay' (function is undefined)
Defining function __phys_addr as symbolic
Defining function find_first_zero_bit as symbolic
Defining function blk_peek_request as symbolic
Defining function blk_rq_map_sg as symbolic
Defining function request_threaded_irq as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'blk_cleanup_queue' (function is undefined)
Defining function del_timer as symbolic
Defining function dev_get_drvdata as symbolic
Defining function pci_enable_device as symbolic
Defining function ioremap_nocache as symbolic
Defining function pci_bus_read_config_dword as symbolic
Defining function pci_bus_read_config_byte as symbolic
Defining function pci_bus_read_config_word as symbolic
Defining function dma_set_mask as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Defining function seq_puts as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function capable as symbolic
Defining function memdup_user as symbolic
Defining function _copy_from_user as symbolic
Defining function _copy_to_user as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.373928070068
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 251 129 702 4471
INFO: Starting verification
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "ida_ioctl" has inline asm
KLEE: WARNING ONCE: function "smart1_completed" has inline asm
KLEE: WARNING ONCE: function "smart1_submit_command" has inline asm
KLEE: WARNING ONCE: function "smart1_intr_mask" has inline asm
KLEE: WARNING ONCE: function "sendcmd" has inline asm
KLEE: WARNING ONCE: function "pci_free_consistent" has inline asm
KLEE: WARNING ONCE: function "cmd_alloc" has inline asm
KLEE: WARNING ONCE: function "do_ida_intr" has inline asm
KLEE: WARNING ONCE: function "do_ida_request" has inline asm
KLEE: WARNING ONCE: function "smart1_fifo_full" has inline asm
KLEE: WARNING ONCE: function "smart1_intr_pending" has inline asm
KLEE: WARNING ONCE: function "smart2e_submit_command" has inline asm
KLEE: WARNING ONCE: function "smart2e_intr_mask" has inline asm
KLEE: WARNING ONCE: function "smart2e_fifo_full" has inline asm
KLEE: WARNING ONCE: function "smart2e_intr_pending" has inline asm
KLEE: WARNING ONCE: function "smart2e_completed" has inline asm
KLEE: WARNING ONCE: function "smart2_submit_command" has inline asm
KLEE: WARNING ONCE: function "smart2_intr_mask" has inline asm
KLEE: WARNING ONCE: function "smart2_fifo_full" has inline asm
KLEE: WARNING ONCE: function "smart2_intr_pending" has inline asm
KLEE: WARNING ONCE: function "smart2_completed" has inline asm
KLEE: WARNING ONCE: function "smart4_submit_command" has inline asm
KLEE: WARNING ONCE: function "smart4_intr_mask" has inline asm
KLEE: WARNING ONCE: function "smart4_fifo_full" has inline asm
KLEE: WARNING ONCE: function "smart4_intr_pending" has inline asm
KLEE: WARNING ONCE: function "smart4_completed" has inline asm
KLEE: WARNING: killing 11791 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 13993 states (over memory cap)
KLEE: WARNING: killing 13875 states (over memory cap)
KLEE: WARNING: killing 14262 states (over memory cap)
KLEE: WARNING: killing 13371 states (over memory cap)
KLEE: WARNING: killing 13504 states (over memory cap)
KLEE: WARNING: killing 13132 states (over memory cap)
KLEE: WARNING: killing 13609 states (over memory cap)
KLEE: WARNING: killing 13661 states (over memory cap)
KLEE: WARNING: killing 14136 states (over memory cap)
KLEE: WARNING: killing 14020 states (over memory cap)
KLEE: WARNING: killing 14164 states (over memory cap)
KLEE: WARNING: killing 13965 states (over memory cap)
KLEE: WARNING: killing 13938 states (over memory cap)
KLEE: WARNING: killing 14413 states (over memory cap)
KLEE: WARNING: killing 14474 states (over memory cap)
KLEE: WARNING: killing 15281 states (over memory cap)
KLEE: WARNING: killing 14759 states (over memory cap)
KLEE: WARNING: killing 14822 states (over memory cap)
KLEE: WARNING: killing 15305 states (over memory cap)
KLEE: WARNING: killing 14945 states (over memory cap)
KLEE: WARNING: killing 15261 states (over memory cap)
KLEE: WARNING: killing 14742 states (over memory cap)
KLEE: WARNING: killing 14803 states (over memory cap)
KLEE: WARNING: killing 14121 states (over memory cap)
KLEE: WARNING: killing 14677 states (over memory cap)
KLEE: WARNING: killing 14490 states (over memory cap)
KLEE: WARNING: killing 13974 states (over memory cap)
KLEE: WARNING: killing 14028 states (over memory cap)
KLEE: WARNING: killing 14330 states (over memory cap)
KLEE: WARNING: killing 14311 states (over memory cap)
KLEE: WARNING: killing 14536 states (over memory cap)
KLEE: WARNING: killing 14511 states (over memory cap)
KLEE: WARNING: killing 14655 states (over memory cap)
KLEE: WARNING: killing 14143 states (over memory cap)
KLEE: WARNING: killing 14039 states (over memory cap)
KLEE: WARNING: killing 14264 states (over memory cap)
KLEE: WARNING: killing 14734 states (over memory cap)
KLEE: WARNING: killing 14223 states (over memory cap)
KLEE: WARNING: killing 14045 states (over memory cap)
KLEE: WARNING: killing 14826 states (over memory cap)
KLEE: WARNING: killing 14726 states (over memory cap)
KLEE: WARNING: killing 14467 states (over memory cap)
KLEE: WARNING: killing 13885 states (over memory cap)
KLEE: WARNING: killing 14427 states (over memory cap)
KLEE: WARNING: killing 14167 states (over memory cap)
KLEE: WARNING: killing 14389 states (over memory cap)
KLEE: WARNING: killing 14688 states (over memory cap)
KLEE: WARNING: killing 14350 states (over memory cap)
KLEE: WARNING: killing 14167 states (over memory cap)
KLEE: WARNING: killing 14712 states (over memory cap)
KLEE: WARNING: killing 14529 states (over memory cap)
KLEE: WARNING: killing 14428 states (over memory cap)
KLEE: WARNING: killing 14092 states (over memory cap)
KLEE: WARNING: killing 13754 states (over memory cap)
KLEE: WARNING: killing 14297 states (over memory cap)
KLEE: WARNING: killing 15064 states (over memory cap)
KLEE: WARNING: killing 14572 states (over memory cap)
KLEE: WARNING: killing 14006 states (over memory cap)
KLEE: WARNING: killing 14534 states (over memory cap)
KLEE: WARNING: killing 14361 states (over memory cap)
KLEE: WARNING: killing 14263 states (over memory cap)
KLEE: WARNING: killing 14559 states (over memory cap)
KLEE: WARNING: killing 14305 states (over memory cap)
KLEE: WARNING: killing 14287 states (over memory cap)
KLEE: WARNING: killing 14422 states (over memory cap)
KLEE: WARNING: killing 14721 states (over memory cap)
KLEE: WARNING: killing 14233 states (over memory cap)
KLEE: WARNING: killing 13899 states (over memory cap)
KLEE: WARNING: killing 13962 states (over memory cap)
KLEE: WARNING: killing 14178 states (over memory cap)
KLEE: WARNING: killing 14629 states (over memory cap)
KLEE: WARNING: killing 14226 states (over memory cap)
KLEE: WARNING: killing 14364 states (over memory cap)
KLEE: WARNING: killing 14575 states (over memory cap)
KLEE: WARNING: killing 14873 states (over memory cap)
KLEE: WARNING: killing 14627 states (over memory cap)
KLEE: WARNING: killing 14528 states (over memory cap)
KLEE: WARNING: killing 14130 states (over memory cap)
KLEE: WARNING: killing 14418 states (over memory cap)
KLEE: WARNING: killing 14091 states (over memory cap)
KLEE: WARNING: killing 13917 states (over memory cap)
KLEE: WARNING: killing 14210 states (over memory cap)
KLEE: WARNING: killing 14424 states (over memory cap)
KLEE: WARNING: killing 13945 states (over memory cap)
KLEE: WARNING: killing 14467 states (over memory cap)
KLEE: WARNING: killing 13987 states (over memory cap)
KLEE: WARNING: killing 14125 states (over memory cap)
KLEE: WARNING: killing 14722 states (over memory cap)
KLEE: WARNING: killing 14012 states (over memory cap)
KLEE: WARNING: killing 14307 states (over memory cap)
KLEE: WARNING: killing 14667 states (over memory cap)
KLEE: WARNING: killing 14576 states (over memory cap)
KLEE: WARNING: killing 14559 states (over memory cap)
KLEE: WARNING: killing 13860 states (over memory cap)
KLEE: WARNING: killing 14221 states (over memory cap)
KLEE: WARNING: killing 13980 states (over memory cap)
KLEE: WARNING: killing 14418 states (over memory cap)
KLEE: WARNING: killing 14250 states (over memory cap)
KLEE: WARNING: killing 14536 states (over memory cap)
KLEE: WARNING: killing 14070 states (over memory cap)
KLEE: WARNING: killing 14508 states (over memory cap)
KLEE: WARNING: killing 14565 states (over memory cap)
KLEE: WARNING: killing 14173 states (over memory cap)
KLEE: WARNING: killing 14082 states (over memory cap)
KLEE: WARNING: killing 14736 states (over memory cap)
KLEE: WARNING: killing 14499 states (over memory cap)
KLEE: WARNING: killing 14030 states (over memory cap)
KLEE: WARNING: killing 14463 states (over memory cap)
KLEE: WARNING: killing 14823 states (over memory cap)
KLEE: WARNING: killing 14288 states (over memory cap)
KLEE: WARNING: killing 15163 states (over memory cap)
KLEE: WARNING: killing 14027 states (over memory cap)
KLEE: WARNING: killing 14084 states (over memory cap)
KLEE: WARNING: killing 14290 states (over memory cap)
KLEE: WARNING: killing 14126 states (over memory cap)
KLEE: WARNING: killing 14182 states (over memory cap)
KLEE: WARNING: killing 14390 states (over memory cap)
KLEE: WARNING: killing 14301 states (over memory cap)
KLEE: WARNING: killing 14362 states (over memory cap)
KLEE: WARNING: killing 14565 states (over memory cap)
KLEE: WARNING: killing 14033 states (over memory cap)
KLEE: WARNING: killing 14382 states (over memory cap)
KLEE: WARNING: killing 14515 states (over memory cap)
KLEE: WARNING: killing 14350 states (over memory cap)
KLEE: WARNING: killing 14411 states (over memory cap)
KLEE: WARNING: killing 14765 states (over memory cap)
KLEE: WARNING: killing 14165 states (over memory cap)
KLEE: WARNING: killing 14147 states (over memory cap)
KLEE: WARNING: killing 13618 states (over memory cap)
KLEE: WARNING: killing 14845 states (over memory cap)
KLEE: WARNING: killing 14401 states (over memory cap)
KLEE: WARNING: killing 14751 states (over memory cap)
KLEE: WARNING: killing 14076 states (over memory cap)
KLEE: WARNING: killing 14061 states (over memory cap)
KLEE: WARNING: killing 13970 states (over memory cap)
KLEE: WARNING: killing 14314 states (over memory cap)
KLEE: WARNING: killing 14008 states (over memory cap)
KLEE: WARNING: killing 14426 states (over memory cap)
KLEE: WARNING: killing 14626 states (over memory cap)
KLEE: WARNING: killing 14323 states (over memory cap)
KLEE: WARNING: killing 14452 states (over memory cap)
KLEE: WARNING: killing 14511 states (over memory cap)
KLEE: WARNING: killing 14132 states (over memory cap)
KLEE: WARNING: killing 14189 states (over memory cap)
KLEE: WARNING: killing 13883 states (over memory cap)
KLEE: WARNING: killing 14227 states (over memory cap)
KLEE: WARNING: killing 14570 states (over memory cap)
KLEE: WARNING: killing 14339 states (over memory cap)
KLEE: WARNING: killing 14110 states (over memory cap)
KLEE: WARNING: killing 14168 states (over memory cap)
KLEE: WARNING: killing 14583 states (over memory cap)
KLEE: WARNING: killing 14782 states (over memory cap)
KLEE: WARNING: killing 14767 states (over memory cap)
KLEE: WARNING: killing 14256 states (over memory cap)
KLEE: WARNING: killing 14891 states (over memory cap)
KLEE: WARNING: killing 14802 states (over memory cap)
