bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13.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.: 19 49 285 2209
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.170715808868
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'unregister_blkdev' (function is undefined)
Removed calls to 'unregister_virtio_driver' (function is undefined)
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 'blk_put_request' (function is undefined)
Defining function blk_make_request as symbolic
Defining function register_blkdev as symbolic
Defining function register_virtio_driver 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
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.140753030777
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 75 46 178 1317
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: ERROR: /tmp/symbiotic-Yn37j9/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13.c:4008: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Yn37j9/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13.c:4050: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Yn37j9/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13.c:3970: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Yn37j9/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13.c:3971: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Yn37j9/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13.c:4050: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Yn37j9/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13.c:4027: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Yn37j9/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13.c:4051: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Yn37j9/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13.c:3971: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Yn37j9/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13.c:3091: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Yn37j9/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13.c:3091: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
