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--block--DAC960.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.: 505 273 3179 25861
Removed infinite loop in dma_map_sg_attrs
Removed infinite loop in sg_page
Removed infinite loop in slice_dma_loaf
Removed infinite loop in DAC960_V2_ProcessCompletedCommand
Removed infinite loop in dma_unmap_sg_attrs
Removed infinite loop in DAC960_V1_ProcessCompletedCommand
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.879231929779
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Defining function vsprintf as symbolic
Defining function printk as symbolic
Defining function check_disk_change as symbolic
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_puts as symbolic
Defining function PDE_DATA as symbolic
Defining function seq_printf as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Defining function simple_strtoul as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Defining function dma_alloc_attrs as symbolic
Defining function _copy_from_user as symbolic
Defining function noop_llseek as symbolic
Removed calls to '__might_sleep' (function is undefined)
Defining function capable as symbolic
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function schedule_timeout as symbolic
Defining function _copy_to_user as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'dma_pool_destroy' (function is undefined)
Removed calls to 'sg_init_table' (function is undefined)
Removed calls to 'dma_pool_free' (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 'blk_queue_max_hw_sectors' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'add_disk' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to 'del_gendisk' (function is undefined)
Removed calls to 'blk_cleanup_queue' (function is undefined)
Removed calls to 'unregister_blkdev' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'put_disk' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function proc_mkdir as symbolic
Defining function sprintf as symbolic
Defining function proc_create_data as symbolic
Removed calls to '__wake_up' (function is undefined)
Defining function register_blkdev as symbolic
Defining function blk_init_queue as symbolic
Removed calls to 'blk_start_request' (function is undefined)
Defining function blk_peek_request as symbolic
Defining function blk_rq_map_sg as symbolic
Removed calls to 'debug_dma_map_sg' (function is undefined)
Defining function sg_next as symbolic
Defining function dma_pool_create as symbolic
Defining function pci_enable_device as symbolic
Defining function alloc_disk as symbolic
Defining function ioremap_nocache as symbolic
Defining function __request_region as symbolic
Defining function request_threaded_irq as symbolic
Defining function strcat as symbolic
Defining function dma_set_mask as symbolic
Removed calls to 'complete' (function is undefined)
Removed calls to 'debug_dma_unmap_sg' (function is undefined)
Defining function __blk_end_request as symbolic
Defining function __memmove 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_2 as symbolic
Defining function ldv_release_15 as symbolic
Defining function ldv_open_10 as symbolic
Defining function ldv_release_10 as symbolic
Defining function misc_register as symbolic
Defining function __pci_register_driver as symbolic
Defining function misc_deregister as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strcmp
  strcpy
  strlen
  strncmp
  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.894796133041
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 607 172 1817 15164
INFO: Starting verification
KLEE: WARNING ONCE: function "DAC960_ExecuteCommand" has inline asm
KLEE: WARNING ONCE: function "DAC960_gam_ioctl" has inline asm
KLEE: WARNING ONCE: function "DAC960_Probe" has inline asm
KLEE: WARNING ONCE: function "DAC960_DetectCleanup" has inline asm
KLEE: WARNING ONCE: function "DAC960_V2_EnableMemoryMailboxInterface" has inline asm
KLEE: WARNING ONCE: function "DAC960_GEM_QueueCommand" has inline asm
KLEE: WARNING ONCE: function "DAC960_BA_QueueCommand" has inline asm
KLEE: WARNING ONCE: function "DAC960_LP_QueueCommand" has inline asm
KLEE: WARNING ONCE: function "DAC960_V1_EnableMemoryMailboxInterface" has inline asm
KLEE: WARNING ONCE: function "DAC960_LA_QueueCommandSingleMode" has inline asm
KLEE: WARNING ONCE: function "DAC960_LA_QueueCommandDualMode" has inline asm
KLEE: WARNING ONCE: function "DAC960_V1_ReadControllerConfiguration" has inline asm
KLEE: WARNING ONCE: function "DAC960_V1_ReadDeviceConfiguration" has inline asm
KLEE: WARNING ONCE: function "DAC960_PG_QueueCommandSingleMode" has inline asm
KLEE: WARNING ONCE: function "DAC960_PG_QueueCommandDualMode" has inline asm
KLEE: WARNING ONCE: function "DAC960_PD_QueueCommand" has inline asm
KLEE: WARNING ONCE: function "DAC960_P_QueueCommand" has inline asm
KLEE: WARNING ONCE: function "pci_map_sg" has inline asm
KLEE: WARNING ONCE: function "slice_dma_loaf" has inline asm
KLEE: WARNING ONCE: function "DAC960_GEM_InterruptHandler" has inline asm
KLEE: WARNING ONCE: function "DAC960_V2_ProcessCompletedCommand" has inline asm
KLEE: WARNING ONCE: function "DAC960_ProcessCompletedRequest" has inline asm
KLEE: WARNING ONCE: function "DAC960_BA_InterruptHandler" has inline asm
KLEE: WARNING ONCE: function "DAC960_LP_InterruptHandler" has inline asm
KLEE: WARNING ONCE: function "DAC960_LA_InterruptHandler" has inline asm
KLEE: WARNING ONCE: function "DAC960_V1_ProcessCompletedCommand" has inline asm
KLEE: WARNING ONCE: function "DAC960_PG_InterruptHandler" has inline asm
KLEE: WARNING ONCE: function "DAC960_PD_InterruptHandler" has inline asm
KLEE: WARNING ONCE: function "DAC960_P_InterruptHandler" has inline asm
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/symbiotic-OD3OwA/linux-4.2-rc1.tar.xz-43_2a-drivers--block--DAC960.ko-entry_point_true-unreach-call.cil.out.c:15701: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_a33290d3-a028-4f8c-a0b7-79a241a14c47/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8973 states (over memory cap)
KLEE: WARNING: killing 16197 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: ERROR: /tmp/symbiotic-OD3OwA/linux-4.2-rc1.tar.xz-43_2a-drivers--block--DAC960.ko-entry_point_true-unreach-call.cil.out.c:13430: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-OD3OwA/linux-4.2-rc1.tar.xz-43_2a-drivers--block--DAC960.ko-entry_point_true-unreach-call.cil.out.c:13590: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-OD3OwA/linux-4.2-rc1.tar.xz-43_2a-drivers--block--DAC960.ko-entry_point_true-unreach-call.cil.out.c:7810: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-OD3OwA/linux-4.2-rc1.tar.xz-43_2a-drivers--block--DAC960.ko-entry_point_true-unreach-call.cil.out.c:13346: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-OD3OwA/linux-4.2-rc1.tar.xz-43_2a-drivers--block--DAC960.ko-entry_point_true-unreach-call.cil.out.c:13472: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-OD3OwA/linux-4.2-rc1.tar.xz-43_2a-drivers--block--DAC960.ko-entry_point_true-unreach-call.cil.out.c:7759: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16933 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-OD3OwA/linux-4.2-rc1.tar.xz-43_2a-drivers--block--DAC960.ko-entry_point_true-unreach-call.cil.out.c:7719: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-OD3OwA/linux-4.2-rc1.tar.xz-43_2a-drivers--block--DAC960.ko-entry_point_true-unreach-call.cil.out.c:13512: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-OD3OwA/linux-4.2-rc1.tar.xz-43_2a-drivers--block--DAC960.ko-entry_point_true-unreach-call.cil.out.c:13553: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17664 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-OD3OwA/linux-4.2-rc1.tar.xz-43_2a-drivers--block--DAC960.ko-entry_point_true-unreach-call.cil.out.c:10730: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-OD3OwA/linux-4.2-rc1.tar.xz-43_2a-drivers--block--DAC960.ko-entry_point_true-unreach-call.cil.out.c:13388: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17510 states (over memory cap)
KLEE: WARNING: killing 18410 states (over memory cap)
KLEE: WARNING: killing 16936 states (over memory cap)
KLEE: WARNING: killing 17940 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-OD3OwA/linux-4.2-rc1.tar.xz-43_2a-drivers--block--DAC960.ko-entry_point_true-unreach-call.cil.out.c:8199: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17355 states (over memory cap)
KLEE: WARNING: killing 18755 states (over memory cap)
KLEE: WARNING: killing 19990 states (over memory cap)
KLEE: WARNING: killing 19797 states (over memory cap)
KLEE: WARNING: killing 20649 states (over memory cap)
KLEE: WARNING: killing 21122 states (over memory cap)
KLEE: WARNING: killing 21049 states (over memory cap)
KLEE: WARNING: killing 19820 states (over memory cap)
KLEE: WARNING: killing 19574 states (over memory cap)
KLEE: WARNING: killing 20531 states (over memory cap)
KLEE: WARNING: killing 20180 states (over memory cap)
KLEE: WARNING: killing 20052 states (over memory cap)
KLEE: WARNING: killing 18771 states (over memory cap)
KLEE: WARNING: killing 19451 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-OD3OwA/linux-4.2-rc1.tar.xz-43_2a-drivers--block--DAC960.ko-entry_point_true-unreach-call.cil.out.c:8199: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 19919 states (over memory cap)
KLEE: WARNING: killing 19998 states (over memory cap)
KLEE: WARNING: killing 18786 states (over memory cap)
KLEE: WARNING: killing 19134 states (over memory cap)
KLEE: WARNING: killing 19325 states (over memory cap)
KLEE: WARNING: killing 20338 states (over memory cap)
KLEE: WARNING: killing 20427 states (over memory cap)
KLEE: WARNING: killing 20078 states (over memory cap)
KLEE: WARNING: killing 20160 states (over memory cap)
KLEE: WARNING: killing 19335 states (over memory cap)
KLEE: WARNING: killing 19688 states (over memory cap)
KLEE: WARNING: killing 19995 states (over memory cap)
KLEE: WARNING: killing 19002 states (over memory cap)
KLEE: WARNING: killing 20054 states (over memory cap)
KLEE: WARNING: killing 20404 states (over memory cap)
KLEE: WARNING: killing 19538 states (over memory cap)
KLEE: WARNING: killing 19300 states (over memory cap)
KLEE: WARNING: killing 20455 states (over memory cap)
KLEE: WARNING: killing 18410 states (over memory cap)
KLEE: WARNING: killing 20142 states (over memory cap)
KLEE: WARNING: killing 20333 states (over memory cap)
KLEE: WARNING: killing 19573 states (over memory cap)
KLEE: WARNING: killing 19660 states (over memory cap)
KLEE: WARNING: killing 19799 states (over memory cap)
KLEE: WARNING: killing 18353 states (over memory cap)
KLEE: WARNING: killing 20383 states (over memory cap)
KLEE: WARNING: killing 19521 states (over memory cap)
KLEE: WARNING: killing 19551 states (over memory cap)
KLEE: WARNING: killing 19688 states (over memory cap)
KLEE: WARNING: killing 20043 states (over memory cap)
KLEE: WARNING: killing 19815 states (over memory cap)
KLEE: WARNING: killing 19641 states (over memory cap)
KLEE: WARNING: killing 19667 states (over memory cap)
KLEE: WARNING: killing 20441 states (over memory cap)
KLEE: WARNING: killing 19159 states (over memory cap)
KLEE: WARNING: killing 19191 states (over memory cap)
KLEE: WARNING: killing 20057 states (over memory cap)
KLEE: WARNING: killing 19727 states (over memory cap)
KLEE: WARNING: killing 20235 states (over memory cap)
KLEE: WARNING: killing 19854 states (over memory cap)
KLEE: WARNING: killing 20151 states (over memory cap)
KLEE: WARNING: killing 19453 states (over memory cap)
KLEE: WARNING: killing 19064 states (over memory cap)
KLEE: WARNING: killing 20404 states (over memory cap)
KLEE: WARNING: killing 20443 states (over memory cap)
KLEE: WARNING: killing 19692 states (over memory cap)
KLEE: WARNING: killing 19105 states (over memory cap)
KLEE: WARNING: killing 19919 states (over memory cap)
KLEE: WARNING: killing 19647 states (over memory cap)
KLEE: WARNING: killing 19317 states (over memory cap)
KLEE: WARNING: killing 20123 states (over memory cap)
KLEE: WARNING: killing 20055 states (over memory cap)
KLEE: WARNING: killing 19991 states (over memory cap)
KLEE: WARNING: killing 18941 states (over memory cap)
KLEE: WARNING: killing 19645 states (over memory cap)
KLEE: WARNING: killing 19833 states (over memory cap)
KLEE: WARNING: killing 19197 states (over memory cap)
KLEE: WARNING: killing 19484 states (over memory cap)
KLEE: WARNING: killing 20444 states (over memory cap)
KLEE: WARNING: killing 19242 states (over memory cap)
KLEE: WARNING: killing 20049 states (over memory cap)
KLEE: WARNING: killing 20799 states (over memory cap)
KLEE: WARNING: killing 19815 states (over memory cap)
KLEE: WARNING: killing 20211 states (over memory cap)
KLEE: WARNING: killing 19835 states (over memory cap)
KLEE: WARNING: killing 19515 states (over memory cap)
KLEE: WARNING: killing 20212 states (over memory cap)
KLEE: WARNING: killing 18663 states (over memory cap)
KLEE: WARNING: killing 20227 states (over memory cap)
KLEE: WARNING: killing 20220 states (over memory cap)
KLEE: WARNING: killing 18827 states (over memory cap)
KLEE: WARNING: killing 19522 states (over memory cap)
KLEE: WARNING: killing 19700 states (over memory cap)
KLEE: WARNING: killing 20095 states (over memory cap)
KLEE: WARNING: killing 20331 states (over memory cap)
KLEE: WARNING: killing 19808 states (over memory cap)
KLEE: WARNING: killing 19846 states (over memory cap)
KLEE: WARNING: killing 19429 states (over memory cap)
KLEE: WARNING: killing 20269 states (over memory cap)
KLEE: WARNING: killing 19800 states (over memory cap)
KLEE: WARNING: killing 20198 states (over memory cap)
KLEE: WARNING: killing 19871 states (over memory cap)
KLEE: WARNING: killing 18948 states (over memory cap)
KLEE: WARNING: killing 19229 states (over memory cap)
KLEE: WARNING: killing 19916 states (over memory cap)
KLEE: WARNING: killing 20356 states (over memory cap)
KLEE: WARNING: killing 19843 states (over memory cap)
KLEE: WARNING: killing 19526 states (over memory cap)
KLEE: WARNING: killing 20356 states (over memory cap)
KLEE: WARNING: killing 19586 states (over memory cap)
KLEE: WARNING: killing 20121 states (over memory cap)
KLEE: WARNING: killing 20863 states (over memory cap)
KLEE: WARNING: killing 19047 states (over memory cap)
KLEE: WARNING: killing 19838 states (over memory cap)
KLEE: WARNING: killing 19872 states (over memory cap)
KLEE: WARNING: killing 18851 states (over memory cap)
KLEE: WARNING: killing 19791 states (over memory cap)
KLEE: WARNING: killing 18672 states (over memory cap)
KLEE: WARNING: killing 19155 states (over memory cap)
KLEE: WARNING: killing 20384 states (over memory cap)
KLEE: WARNING: killing 19528 states (over memory cap)
KLEE: WARNING: killing 19707 states (over memory cap)
KLEE: WARNING: killing 20737 states (over memory cap)
KLEE: WARNING: killing 19730 states (over memory cap)
KLEE: WARNING: killing 21359 states (over memory cap)
KLEE: WARNING: killing 19554 states (over memory cap)
KLEE: WARNING: killing 19093 states (over memory cap)
KLEE: WARNING: killing 18618 states (over memory cap)
KLEE: WARNING: killing 19641 states (over memory cap)
