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-08_1a-drivers--block--loop.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.: 99 181 1387 8776
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.444470882416
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function idr_for_each as symbolic
Removed calls to '___might_sleep' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function _cond_resched as symbolic
Removed calls to 'blk_mq_start_request' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Defining function blk_mq_map_queue as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Removed calls to 'zero_fill_bio' (function is undefined)
Removed calls to 'iov_iter_bvec' (function is undefined)
Removed calls to 'blk_mq_complete_request' (function is undefined)
Defining function vfs_iter_read as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function ___ratelimit as symbolic
Defining function printk as symbolic
Defining function alloc_pages_current as symbolic
Removed calls to '__sb_end_write' (function is undefined)
Defining function vfs_iter_write as symbolic
Defining function __sb_start_write as symbolic
Defining function vfs_fsync as symbolic
Defining function queue_work_on as symbolic
Removed calls to 'blk_mq_freeze_queue' (function is undefined)
Removed calls to 'blk_mq_unfreeze_queue' (function is undefined)
Removed calls to 'set_device_ro' (function is undefined)
Removed calls to 'blk_queue_flush' (function is undefined)
Removed calls to 'bd_set_size' (function is undefined)
Removed calls to 'fput' (function is undefined)
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function vfs_getattr as symbolic
Defining function capable as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function __blkdev_reread_part as symbolic
Defining function blkdev_reread_part as symbolic
Defining function kobject_uevent as symbolic
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function _copy_from_user as symbolic
Removed calls to 'bdput' (function is undefined)
Removed calls to 'invalidate_bdev' (function is undefined)
Removed calls to 'sysfs_remove_group' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Defining function fget as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function set_blocksize as symbolic
Defining function bdgrab as symbolic
Defining function sysfs_create_group as symbolic
Defining function noop_llseek as symbolic
Removed calls to 'idr_remove' (function is undefined)
Defining function nonseekable_open as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'add_disk' (function is undefined)
Removed calls to 'blk_cleanup_queue' (function is undefined)
Removed calls to 'blk_mq_free_tag_set' (function is undefined)
Removed calls to 'del_gendisk' (function is undefined)
Removed calls to 'put_disk' (function is undefined)
Defining function idr_alloc as symbolic
Defining function blk_mq_alloc_tag_set as symbolic
Defining function blk_mq_init_queue as symbolic
Defining function alloc_disk as symbolic
Defining function sprintf as symbolic
Defining function idr_find_slowpath as symbolic
Defining function file_path as symbolic
Defining function __memmove as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'idr_destroy' (function is undefined)
Removed calls to 'blk_unregister_region' (function is undefined)
Removed calls to 'unregister_blkdev' (function is undefined)
Removed calls to 'blk_register_region' (function is undefined)
Defining function ldv_setup_11 as symbolic
Defining function ldv_release_11 as symbolic
Defining function ldv_release_3 as symbolic
Defining function register_blkdev as symbolic
Defining function misc_deregister as symbolic
Defining function get_disk as symbolic
Defining function misc_register as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Linked our definitions to these undefined functions:
  strlen
  __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.661833047867
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 200 142 745 10479
INFO: Starting verification
KLEE: WARNING ONCE: function "transfer_xor" has inline asm
KLEE: WARNING ONCE: function "__kunmap_atomic" has inline asm
KLEE: WARNING ONCE: function "lo_open" has inline asm
KLEE: WARNING ONCE: function "lo_release" has inline asm
KLEE: WARNING ONCE: function "loop_set_status" has inline asm
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_189b1508-3005-4cc6-b066-1311a4f6eef8/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-ALJf8T/linux-4.2-rc1.tar.xz-08_1a-drivers--block--loop.ko-entry_point_false-unreach-call.cil.out.c:7363: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11497 states (over memory cap)
KLEE: WARNING: killing 14770 states (over memory cap)
KLEE: WARNING: killing 14659 states (over memory cap)
KLEE: WARNING: killing 15149 states (over memory cap)
KLEE: WARNING: killing 13319 states (over memory cap)
KLEE: WARNING: killing 12988 states (over memory cap)
KLEE: WARNING: killing 14071 states (over memory cap)
KLEE: WARNING: killing 14416 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 14538 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-ALJf8T/linux-4.2-rc1.tar.xz-08_1a-drivers--block--loop.ko-entry_point_false-unreach-call.cil.out.c:4360: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-ALJf8T/linux-4.2-rc1.tar.xz-08_1a-drivers--block--loop.ko-entry_point_false-unreach-call.cil.out.c:6796: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-ALJf8T/linux-4.2-rc1.tar.xz-08_1a-drivers--block--loop.ko-entry_point_false-unreach-call.cil.out.c:7035: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-ALJf8T/linux-4.2-rc1.tar.xz-08_1a-drivers--block--loop.ko-entry_point_false-unreach-call.cil.out.c:5956: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-ALJf8T/linux-4.2-rc1.tar.xz-08_1a-drivers--block--loop.ko-entry_point_false-unreach-call.cil.out.c:6997: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14508 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-ALJf8T/linux-4.2-rc1.tar.xz-08_1a-drivers--block--loop.ko-entry_point_false-unreach-call.cil.out.c:5956: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15292 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-ALJf8T/linux-4.2-rc1.tar.xz-08_1a-drivers--block--loop.ko-entry_point_false-unreach-call.cil.out.c:5956: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15038 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-ALJf8T/linux-4.2-rc1.tar.xz-08_1a-drivers--block--loop.ko-entry_point_false-unreach-call.cil.out.c:7166: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-ALJf8T/linux-4.2-rc1.tar.xz-08_1a-drivers--block--loop.ko-entry_point_false-unreach-call.cil.out.c:6007: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15305 states (over memory cap)
KLEE: WARNING: killing 15723 states (over memory cap)
KLEE: WARNING: killing 16438 states (over memory cap)
KLEE: WARNING: killing 16608 states (over memory cap)
KLEE: WARNING: killing 16144 states (over memory cap)
KLEE: WARNING: killing 15977 states (over memory cap)
KLEE: WARNING: killing 17122 states (over memory cap)
KLEE: WARNING: killing 16301 states (over memory cap)
KLEE: WARNING: killing 16726 states (over memory cap)
KLEE: WARNING: killing 16122 states (over memory cap)
KLEE: WARNING: killing 15883 states (over memory cap)
KLEE: WARNING: killing 15787 states (over memory cap)
KLEE: WARNING: killing 16280 states (over memory cap)
KLEE: WARNING: killing 16258 states (over memory cap)
KLEE: WARNING: killing 15442 states (over memory cap)
KLEE: WARNING: killing 15786 states (over memory cap)
KLEE: WARNING: killing 15693 states (over memory cap)
KLEE: WARNING: killing 15954 states (over memory cap)
KLEE: WARNING: killing 15724 states (over memory cap)
KLEE: WARNING: killing 15408 states (over memory cap)
KLEE: WARNING: killing 15820 states (over memory cap)
KLEE: WARNING: killing 15586 states (over memory cap)
KLEE: WARNING: killing 15926 states (over memory cap)
KLEE: WARNING: killing 15615 states (over memory cap)
KLEE: WARNING: killing 16098 states (over memory cap)
KLEE: WARNING: killing 15646 states (over memory cap)
KLEE: WARNING: killing 15701 states (over memory cap)
KLEE: WARNING: killing 15964 states (over memory cap)
KLEE: WARNING: killing 15729 states (over memory cap)
KLEE: WARNING: killing 15644 states (over memory cap)
KLEE: WARNING: killing 16194 states (over memory cap)
KLEE: WARNING: killing 15112 states (over memory cap)
KLEE: WARNING: killing 15584 states (over memory cap)
KLEE: WARNING: killing 15710 states (over memory cap)
KLEE: WARNING: killing 16191 states (over memory cap)
KLEE: WARNING: killing 16175 states (over memory cap)
KLEE: WARNING: killing 15869 states (over memory cap)
KLEE: WARNING: killing 15642 states (over memory cap)
KLEE: WARNING: killing 15697 states (over memory cap)
KLEE: WARNING: killing 15681 states (over memory cap)
KLEE: WARNING: killing 16013 states (over memory cap)
KLEE: WARNING: killing 15782 states (over memory cap)
KLEE: WARNING: killing 15340 states (over memory cap)
KLEE: WARNING: killing 15881 states (over memory cap)
KLEE: WARNING: killing 16494 states (over memory cap)
KLEE: WARNING: killing 15991 states (over memory cap)
KLEE: WARNING: killing 15345 states (over memory cap)
KLEE: WARNING: killing 15192 states (over memory cap)
KLEE: WARNING: killing 16144 states (over memory cap)
KLEE: WARNING: killing 15080 states (over memory cap)
KLEE: WARNING: killing 16314 states (over memory cap)
KLEE: WARNING: killing 15949 states (over memory cap)
KLEE: WARNING: killing 15655 states (over memory cap)
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_189b1508-3005-4cc6-b066-1311a4f6eef8/symbiotic/lib/libc/strlen.c:6: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15783 states (over memory cap)
KLEE: WARNING: killing 16597 states (over memory cap)
KLEE: WARNING: killing 16175 states (over memory cap)
KLEE: WARNING: killing 16013 states (over memory cap)
KLEE: WARNING: killing 15996 states (over memory cap)
KLEE: WARNING: killing 15498 states (over memory cap)
KLEE: WARNING: killing 15417 states (over memory cap)
KLEE: WARNING: killing 15602 states (over memory cap)
KLEE: WARNING: killing 15789 states (over memory cap)
KLEE: WARNING: killing 15154 states (over memory cap)
KLEE: WARNING: killing 15893 states (over memory cap)
KLEE: WARNING: killing 15602 states (over memory cap)
KLEE: WARNING: killing 16138 states (over memory cap)
KLEE: WARNING: killing 14753 states (over memory cap)
KLEE: WARNING: killing 15485 states (over memory cap)
KLEE: WARNING: killing 16624 states (over memory cap)
KLEE: WARNING: killing 15664 states (over memory cap)
KLEE: WARNING: killing 15777 states (over memory cap)
KLEE: WARNING: killing 15772 states (over memory cap)
KLEE: WARNING: killing 15819 states (over memory cap)
KLEE: WARNING: killing 16351 states (over memory cap)
KLEE: WARNING: killing 15927 states (over memory cap)
KLEE: WARNING: killing 15647 states (over memory cap)
KLEE: WARNING: killing 16237 states (over memory cap)
KLEE: WARNING: killing 15749 states (over memory cap)
KLEE: WARNING: killing 15607 states (over memory cap)
KLEE: WARNING: killing 15593 states (over memory cap)
KLEE: WARNING: killing 16314 states (over memory cap)
KLEE: WARNING: killing 15495 states (over memory cap)
KLEE: WARNING: killing 16695 states (over memory cap)
KLEE: WARNING: killing 15875 states (over memory cap)
KLEE: WARNING: killing 15520 states (over memory cap)
KLEE: WARNING: killing 15438 states (over memory cap)
KLEE: WARNING: killing 15691 states (over memory cap)
KLEE: WARNING: killing 14936 states (over memory cap)
KLEE: WARNING: killing 16000 states (over memory cap)
KLEE: WARNING: killing 15643 states (over memory cap)
KLEE: WARNING: killing 16159 states (over memory cap)
KLEE: WARNING: killing 16552 states (over memory cap)
KLEE: WARNING: killing 16271 states (over memory cap)
KLEE: WARNING: killing 15389 states (over memory cap)
KLEE: WARNING: killing 15503 states (over memory cap)
KLEE: WARNING: killing 15961 states (over memory cap)
KLEE: WARNING: killing 16015 states (over memory cap)
KLEE: WARNING: killing 15333 states (over memory cap)
KLEE: WARNING: killing 16245 states (over memory cap)
KLEE: WARNING: killing 16501 states (over memory cap)
KLEE: WARNING: killing 16090 states (over memory cap)
KLEE: WARNING: killing 15212 states (over memory cap)
KLEE: WARNING: killing 15394 states (over memory cap)
KLEE: WARNING: killing 16236 states (over memory cap)
KLEE: WARNING: killing 15829 states (over memory cap)
KLEE: WARNING: killing 16350 states (over memory cap)
KLEE: WARNING: killing 15807 states (over memory cap)
KLEE: WARNING: killing 15529 states (over memory cap)
KLEE: WARNING: killing 15318 states (over memory cap)
KLEE: WARNING: killing 16223 states (over memory cap)
KLEE: WARNING: killing 16151 states (over memory cap)
KLEE: WARNING: killing 15544 states (over memory cap)
KLEE: WARNING: killing 15592 states (over memory cap)
KLEE: WARNING: killing 15388 states (over memory cap)
KLEE: WARNING: killing 16024 states (over memory cap)
KLEE: WARNING: killing 15944 states (over memory cap)
KLEE: WARNING: killing 15802 states (over memory cap)
KLEE: WARNING: killing 15857 states (over memory cap)
KLEE: WARNING: killing 15645 states (over memory cap)
KLEE: WARNING: killing 15303 states (over memory cap)
KLEE: WARNING: killing 15422 states (over memory cap)
KLEE: WARNING: killing 15675 states (over memory cap)
KLEE: WARNING: killing 15467 states (over memory cap)
KLEE: WARNING: killing 16495 states (over memory cap)
KLEE: WARNING: killing 16224 states (over memory cap)
KLEE: WARNING: killing 14777 states (over memory cap)
KLEE: WARNING: killing 15867 states (over memory cap)
KLEE: WARNING: killing 15600 states (over memory cap)
KLEE: WARNING: killing 16045 states (over memory cap)
KLEE: WARNING: killing 16154 states (over memory cap)
KLEE: WARNING: killing 16215 states (over memory cap)
KLEE: WARNING: killing 15677 states (over memory cap)
KLEE: WARNING: killing 15534 states (over memory cap)
KLEE: WARNING: killing 15972 states (over memory cap)
KLEE: WARNING: killing 15826 states (over memory cap)
KLEE: WARNING: killing 15428 states (over memory cap)
KLEE: WARNING: killing 15087 states (over memory cap)
KLEE: WARNING: killing 15975 states (over memory cap)
KLEE: WARNING: killing 15835 states (over memory cap)
KLEE: WARNING: killing 16211 states (over memory cap)
KLEE: WARNING: killing 15868 states (over memory cap)
KLEE: WARNING: killing 16046 states (over memory cap)
KLEE: WARNING: killing 16228 states (over memory cap)
KLEE: WARNING: killing 15959 states (over memory cap)
KLEE: WARNING: killing 15502 states (over memory cap)
KLEE: WARNING: killing 16127 states (over memory cap)
KLEE: WARNING: killing 15151 states (over memory cap)
KLEE: WARNING: killing 15394 states (over memory cap)
KLEE: WARNING: killing 16090 states (over memory cap)
KLEE: WARNING: killing 15815 states (over memory cap)
KLEE: WARNING: killing 15547 states (over memory cap)
KLEE: WARNING: killing 15344 states (over memory cap)
KLEE: WARNING: killing 15201 states (over memory cap)
KLEE: WARNING: killing 15758 states (over memory cap)
