bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-validator-v0.8/linux-stable-39a1d13-1-101_1a-drivers--block--virtio_blk.ko-entry_point_ldv-val-v0.8_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 359 2477
Removed infinite loop in ldv_stop
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
INFO: Compilation, preparation and instrumentation time: 0.198006868362
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_ulong_named
INFO: After-slicing optimizations and preparation time: 0.220545053482
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 86 58 217 1538
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_a7d04e81-a4f6-47cf-8027-895a94d18d00/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-4FowI4/linux-stable-39a1d13-1-101_1a-drivers--block--virtio_blk.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:3792: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-4FowI4/linux-stable-39a1d13-1-101_1a-drivers--block--virtio_blk.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:3871: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-4FowI4/linux-stable-39a1d13-1-101_1a-drivers--block--virtio_blk.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:3089: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 12808 states (over memory cap)
KLEE: WARNING: killing 12488 states (over memory cap)
KLEE: WARNING: killing 12514 states (over memory cap)
KLEE: WARNING: killing 12324 states (over memory cap)
KLEE: WARNING: killing 12915 states (over memory cap)
KLEE: WARNING: killing 12849 states (over memory cap)
KLEE: WARNING: killing 13108 states (over memory cap)
KLEE: WARNING: killing 13045 states (over memory cap)
KLEE: WARNING: killing 12990 states (over memory cap)
KLEE: WARNING: killing 13467 states (over memory cap)
KLEE: WARNING: killing 13414 states (over memory cap)
KLEE: WARNING: killing 13581 states (over memory cap)
KLEE: WARNING: killing 13525 states (over memory cap)
KLEE: WARNING: killing 13787 states (over memory cap)
KLEE: WARNING: killing 13737 states (over memory cap)
KLEE: WARNING: killing 13575 states (over memory cap)
KLEE: WARNING: killing 10588 states (over memory cap)
KLEE: WARNING: killing 10556 states (over memory cap)
KLEE: WARNING: killing 13771 states (over memory cap)
KLEE: WARNING: killing 10598 states (over memory cap)
KLEE: WARNING: killing 13476 states (over memory cap)
KLEE: WARNING: killing 11158 states (over memory cap)
KLEE: WARNING: killing 10808 states (over memory cap)
KLEE: WARNING: killing 10684 states (over memory cap)
KLEE: WARNING: killing 10764 states (over memory cap)
KLEE: WARNING: killing 10526 states (over memory cap)
KLEE: WARNING: killing 10802 states (over memory cap)
KLEE: WARNING: killing 10878 states (over memory cap)
KLEE: WARNING: killing 10952 states (over memory cap)
KLEE: WARNING: killing 10822 states (over memory cap)
KLEE: WARNING: killing 10690 states (over memory cap)
KLEE: WARNING: killing 10861 states (over memory cap)
KLEE: WARNING: killing 10936 states (over memory cap)
KLEE: WARNING: killing 11016 states (over memory cap)
KLEE: WARNING: killing 10680 states (over memory cap)
KLEE: WARNING: killing 10850 states (over memory cap)
KLEE: WARNING: killing 10916 states (over memory cap)
KLEE: WARNING: killing 11090 states (over memory cap)
KLEE: WARNING: killing 11159 states (over memory cap)
KLEE: WARNING: killing 10937 states (over memory cap)
KLEE: WARNING: killing 11009 states (over memory cap)
KLEE: WARNING: killing 11181 states (over memory cap)
KLEE: WARNING: killing 10852 states (over memory cap)
KLEE: WARNING: killing 11418 states (over memory cap)
KLEE: WARNING: killing 11001 states (over memory cap)
KLEE: WARNING: killing 11064 states (over memory cap)
KLEE: WARNING: killing 11139 states (over memory cap)
KLEE: WARNING: killing 11118 states (over memory cap)
KLEE: WARNING: killing 10792 states (over memory cap)
KLEE: WARNING: killing 11349 states (over memory cap)
KLEE: WARNING: killing 10829 states (over memory cap)
KLEE: WARNING: killing 11188 states (over memory cap)
KLEE: WARNING: killing 11155 states (over memory cap)
KLEE: WARNING: killing 10939 states (over memory cap)
KLEE: WARNING: killing 11294 states (over memory cap)
KLEE: WARNING: killing 11175 states (over memory cap)
KLEE: WARNING: killing 10951 states (over memory cap)
KLEE: WARNING: killing 11019 states (over memory cap)
KLEE: WARNING: killing 11377 states (over memory cap)
KLEE: WARNING: killing 11250 states (over memory cap)
KLEE: WARNING: killing 11124 states (over memory cap)
KLEE: WARNING: killing 11194 states (over memory cap)
KLEE: WARNING: killing 11359 states (over memory cap)
KLEE: WARNING: killing 11331 states (over memory cap)
KLEE: WARNING: killing 11211 states (over memory cap)
KLEE: WARNING: killing 11282 states (over memory cap)
KLEE: WARNING: killing 10788 states (over memory cap)
KLEE: WARNING: killing 11040 states (over memory cap)
KLEE: WARNING: killing 11107 states (over memory cap)
KLEE: WARNING: killing 10986 states (over memory cap)
KLEE: WARNING: killing 11060 states (over memory cap)
KLEE: WARNING: killing 11217 states (over memory cap)
KLEE: WARNING: killing 10913 states (over memory cap)
KLEE: WARNING: killing 11158 states (over memory cap)
KLEE: WARNING: killing 11221 states (over memory cap)
KLEE: WARNING: killing 10925 states (over memory cap)
KLEE: WARNING: killing 10986 states (over memory cap)
KLEE: WARNING: killing 11055 states (over memory cap)
KLEE: WARNING: killing 11321 states (over memory cap)
