bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-validator-v0.6/linux-stable-39a1d13-1-101_1a-drivers--block--virtio_blk.ko-entry_point_false-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.: 27 59 361 2460
Removed infinite loop in ldv_stop___0
Removed infinite loop in virtblk_remove
Removed infinite loop in do_virtblk_request
Removed infinite loop in do_req
Removed infinite loop in sg_assign_page
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.178686141968
Removed calls to 'bio_put' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'virtio_check_driver_offered_feature' (function is undefined)
Defining function scsi_cmd_ioctl as symbolic
Defining function _copy_to_user as symbolic
Defining function bio_map_kern as symbolic
Defining function blk_execute_rq as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'sg_init_table' (function is undefined)
Removed calls to 'put_disk' (function is undefined)
Removed calls to 'set_disk_ro' (function is undefined)
Removed calls to 'blk_queue_max_segments' (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_max_segment_size' (function is undefined)
Removed calls to 'blk_queue_logical_block_size' (function is undefined)
Removed calls to 'blk_queue_physical_block_size' (function is undefined)
Removed calls to 'blk_queue_alignment_offset' (function is undefined)
Removed calls to 'blk_queue_io_min' (function is undefined)
Removed calls to 'blk_queue_io_opt' (function is undefined)
Removed calls to 'add_disk' (function is undefined)
Removed calls to 'mempool_destroy' (function is undefined)
Removed calls to 'del_gendisk' (function is undefined)
Removed calls to 'blk_cleanup_queue' (function is undefined)
Removed calls to '__blk_end_request_all' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'mempool_free' (function is undefined)
Removed calls to 'blk_start_queue' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function alloc_disk as symbolic
Removed calls to 'blk_stop_queue' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'blk_start_request' (function is undefined)
Removed calls to 'virtqueue_kick' (function is undefined)
Defining function blk_init_queue as symbolic
Defining function sprintf as symbolic
Defining function blk_queue_ordered as symbolic
Defining function blk_peek_request as symbolic
Defining function mempool_alloc as symbolic
Defining function blk_rq_map_sg as symbolic
Defining function virtqueue_add_buf_gfp as symbolic
Defining function __phys_addr as symbolic
Defining function mempool_kmalloc as symbolic
Defining function mempool_create as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function virtqueue_get_buf as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'unregister_blkdev' (function is undefined)
Removed calls to 'unregister_virtio_driver' (function is undefined)
Defining function register_blkdev as symbolic
Defining function register_virtio_driver 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_uint_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.209897041321
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 89 60 219 1514
INFO: Starting verification
KLEE: WARNING ONCE: function "virtblk_ioctl" has inline asm
KLEE: WARNING ONCE: function "virtblk_getgeo" has inline asm
KLEE: WARNING ONCE: function "virtblk_probe" has inline asm
KLEE: WARNING ONCE: function "virtblk_remove" has inline asm
KLEE: WARNING ONCE: function "do_virtblk_request" has inline asm
KLEE: WARNING ONCE: function "sg_set_buf" has inline asm
KLEE: WARNING: undefined reference to function: mempool_kfree
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_ef36cf32-d0e2-4f9e-9d80-e0ee2b94f412/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wF2_tr/linux-stable-39a1d13-1-101_1a-drivers--block--virtio_blk.ko-entry_point_false-unreach-call.cil.out.c:4158: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wF2_tr/linux-stable-39a1d13-1-101_1a-drivers--block--virtio_blk.ko-entry_point_false-unreach-call.cil.out.c:4116: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wF2_tr/linux-stable-39a1d13-1-101_1a-drivers--block--virtio_blk.ko-entry_point_false-unreach-call.cil.out.c:3089: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wF2_tr/linux-stable-39a1d13-1-101_1a-drivers--block--virtio_blk.ko-entry_point_false-unreach-call.cil.out.c:4158: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wF2_tr/linux-stable-39a1d13-1-101_1a-drivers--block--virtio_blk.ko-entry_point_false-unreach-call.cil.out.c:4079: 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 12431 states (over memory cap)
KLEE: WARNING: killing 12550 states (over memory cap)
KLEE: WARNING: killing 12238 states (over memory cap)
KLEE: WARNING: killing 12265 states (over memory cap)
KLEE: WARNING: killing 12501 states (over memory cap)
KLEE: WARNING: killing 12316 states (over memory cap)
KLEE: WARNING: killing 12458 states (over memory cap)
KLEE: WARNING: killing 12609 states (over memory cap)
KLEE: WARNING: killing 12651 states (over memory cap)
KLEE: WARNING: killing 13007 states (over memory cap)
KLEE: WARNING: killing 12947 states (over memory cap)
KLEE: WARNING: killing 13196 states (over memory cap)
KLEE: WARNING: killing 12730 states (over memory cap)
KLEE: WARNING: killing 12986 states (over memory cap)
KLEE: WARNING: killing 12833 states (over memory cap)
KLEE: WARNING: killing 13189 states (over memory cap)
KLEE: WARNING: killing 12730 states (over memory cap)
KLEE: WARNING: killing 13094 states (over memory cap)
KLEE: WARNING: killing 10124 states (over memory cap)
KLEE: WARNING: killing 12492 states (over memory cap)
KLEE: WARNING: killing 10155 states (over memory cap)
KLEE: WARNING: killing 12615 states (over memory cap)
KLEE: WARNING: killing 12770 states (over memory cap)
KLEE: WARNING: killing 10255 states (over memory cap)
KLEE: WARNING: killing 9930 states (over memory cap)
KLEE: WARNING: killing 9909 states (over memory cap)
KLEE: WARNING: killing 9981 states (over memory cap)
KLEE: WARNING: killing 9854 states (over memory cap)
KLEE: WARNING: killing 10126 states (over memory cap)
KLEE: WARNING: killing 10098 states (over memory cap)
KLEE: WARNING: killing 9978 states (over memory cap)
KLEE: WARNING: killing 9949 states (over memory cap)
KLEE: WARNING: killing 9733 states (over memory cap)
KLEE: WARNING: killing 9804 states (over memory cap)
KLEE: WARNING: killing 9878 states (over memory cap)
KLEE: WARNING: killing 10046 states (over memory cap)
KLEE: WARNING: killing 10218 states (over memory cap)
KLEE: WARNING: killing 10095 states (over memory cap)
KLEE: WARNING: killing 9776 states (over memory cap)
KLEE: WARNING: killing 10132 states (over memory cap)
KLEE: WARNING: killing 10013 states (over memory cap)
KLEE: WARNING: killing 10178 states (over memory cap)
KLEE: WARNING: killing 10061 states (over memory cap)
KLEE: WARNING: killing 10127 states (over memory cap)
KLEE: WARNING: killing 9814 states (over memory cap)
KLEE: WARNING: killing 9978 states (over memory cap)
KLEE: WARNING: killing 10241 states (over memory cap)
KLEE: WARNING: killing 9937 states (over memory cap)
KLEE: WARNING: killing 9817 states (over memory cap)
KLEE: WARNING: killing 9980 states (over memory cap)
KLEE: WARNING: killing 10334 states (over memory cap)
KLEE: WARNING: killing 10121 states (over memory cap)
KLEE: WARNING: killing 10287 states (over memory cap)
KLEE: WARNING: killing 10168 states (over memory cap)
KLEE: WARNING: killing 10234 states (over memory cap)
KLEE: WARNING: killing 10035 states (over memory cap)
KLEE: WARNING: killing 10017 states (over memory cap)
KLEE: WARNING: killing 10452 states (over memory cap)
KLEE: WARNING: killing 10155 states (over memory cap)
KLEE: WARNING: killing 9945 states (over memory cap)
KLEE: WARNING: killing 10194 states (over memory cap)
KLEE: WARNING: killing 10355 states (over memory cap)
KLEE: WARNING: killing 10324 states (over memory cap)
KLEE: WARNING: killing 10127 states (over memory cap)
KLEE: WARNING: killing 10011 states (over memory cap)
KLEE: WARNING: killing 10350 states (over memory cap)
KLEE: WARNING: killing 9779 states (over memory cap)
KLEE: WARNING: killing 10122 states (over memory cap)
KLEE: WARNING: killing 10192 states (over memory cap)
KLEE: WARNING: killing 10528 states (over memory cap)
KLEE: WARNING: killing 10245 states (over memory cap)
KLEE: WARNING: killing 10753 states (over memory cap)
KLEE: WARNING: killing 10203 states (over memory cap)
KLEE: WARNING: killing 10541 states (over memory cap)
KLEE: WARNING: killing 10334 states (over memory cap)
KLEE: WARNING: killing 10219 states (over memory cap)
KLEE: WARNING: killing 10196 states (over memory cap)
KLEE: WARNING: killing 10083 states (over memory cap)
KLEE: WARNING: killing 10411 states (over memory cap)
KLEE: WARNING: killing 10221 states (over memory cap)
KLEE: WARNING: killing 10457 states (over memory cap)
KLEE: WARNING: killing 10255 states (over memory cap)
KLEE: WARNING: killing 10318 states (over memory cap)
KLEE: WARNING: killing 10306 states (over memory cap)
