bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_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.: 72 365 2223 17751
Removed infinite loop in node_prepare_for_write
Removed infinite loop in sm_disk_new_block
Removed infinite loop in dm_btree_remove
Removed infinite loop in shadow_current
Removed infinite loop in __find_holder
Removed infinite loop in shadow_parent
Removed infinite loop in dm_tm_inc
Removed infinite loop in delete_at
Removed infinite loop in dm_tm_dec
Removed infinite loop in __rebalance3
Removed infinite loop in delete_center_node
Removed infinite loop in redistribute3
Removed infinite loop in shift
Removed infinite loop in node_shift
Removed infinite loop in node_copy
Removed infinite loop in bl_up_read
Removed infinite loop in __wake_many
Removed infinite loop in ro_node
Removed infinite loop in trim_ablock
Removed infinite loop in fill_ablock
Removed infinite loop in dm_btree_walk
Removed infinite loop in ro_pop
INFO: Compilation, preparation and instrumentation time: 0.619745016098
Defining function ___ratelimit as symbolic
Defining function printk as symbolic
Defining function crc32c as symbolic
Defining function dm_bufio_get_block_number as symbolic
Defining function dm_bufio_get_block_data as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function dm_bufio_get_block_size as symbolic
Removed calls to 'dm_bufio_release' (function is undefined)
Defining function dm_bufio_new as symbolic
Defining function dm_bufio_get_aux_data as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to 'print_stack_trace' (function is undefined)
Removed calls to 'save_stack_trace' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to '__put_task_struct' (function is undefined)
Defining function dm_bufio_read as symbolic
Removed calls to 'list_del' (function is undefined)
Defining function wake_up_process as symbolic
Defining function dm_bufio_get as symbolic
Removed calls to 'dm_bufio_mark_buffer_dirty' (function is undefined)
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function dm_bufio_client_create as symbolic
Defining function dm_bufio_get_client as symbolic
Removed calls to 'dm_bufio_client_destroy' (function is undefined)
Defining function dm_bufio_get_device_size as symbolic
Defining function dm_bufio_write_dirty_buffers as symbolic
Linked our definitions to these undefined functions:
  memcmp
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.617700099945
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 180 285 1434 10803
INFO: Starting verification
KLEE: WARNING ONCE: function "node_prepare_for_write" has inline asm
KLEE: WARNING ONCE: function "sm_disk_new_block" has inline asm
KLEE: WARNING ONCE: function "sm_ll_find_free_block" has inline asm
KLEE: WARNING ONCE: function "sm_ll_insert" has inline asm
KLEE: WARNING ONCE: function "dm_btree_remove" has inline asm
KLEE: WARNING ONCE: function "shadow_current" has inline asm
KLEE: WARNING ONCE: function "shadow_parent" has inline asm
KLEE: WARNING ONCE: function "bl_down_write" has inline asm
KLEE: WARNING ONCE: function "__check_holder" has inline asm
KLEE: WARNING ONCE: function "__add_holder" has inline asm
KLEE: WARNING ONCE: function "__wait" has inline asm
KLEE: WARNING ONCE: function "put_task_struct" has inline asm
KLEE: WARNING ONCE: function "__find_holder" has inline asm
KLEE: WARNING ONCE: function "dm_tm_inc" has inline asm
KLEE: WARNING ONCE: function "delete_at" has inline asm
KLEE: WARNING ONCE: function "dm_tm_dec" has inline asm
KLEE: WARNING ONCE: function "node_copy" has inline asm
KLEE: WARNING ONCE: function "node_shift" has inline asm
KLEE: WARNING ONCE: function "shift" has inline asm
KLEE: WARNING ONCE: function "dm_bm_read_try_lock" has inline asm
KLEE: WARNING ONCE: function "dm_bm_read_lock" has inline asm
KLEE: WARNING ONCE: function "bl_up_read" has inline asm
KLEE: WARNING ONCE: function "__wake_many" has inline asm
KLEE: WARNING ONCE: function "bl_up_write" has inline asm
KLEE: WARNING ONCE: function "sm_ll_lookup_bitmap" has inline asm
KLEE: WARNING ONCE: function "ro_node" has inline asm
KLEE: WARNING ONCE: function "shrink" has inline asm
KLEE: WARNING ONCE: function "fill_ablock" has inline asm
KLEE: WARNING ONCE: function "dm_btree_walk" has inline asm
KLEE: WARNING ONCE: function "ro_pop" has inline asm
KLEE: WARNING ONCE: function "dm_bitset_set_bit" has inline asm
KLEE: WARNING ONCE: function "dm_bitset_clear_bit" has inline asm
KLEE: WARNING ONCE: function "dm_bitset_test_bit" has inline asm
KLEE: WARNING ONCE: flushing 9592 bytes on read, may be slow and/or crash: MO58[9592] allocated at global:
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6224: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6144: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6144: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6204: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6204: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6145: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6239: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6205: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6164: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6179: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
klee: /var/xchalup4/symbiotic/klee/lib/Core/SpecialFunctionHandler.cpp:250: std::__cxx11::string klee::SpecialFunctionHandler::readStringAtAddress(klee::ExecutionState&, klee::ref<klee::Expr>): Assertion `isa<ConstantExpr>(cur) && "hit symbolic char while reading concrete string"' failed.
KLEE: output directory is "/tmp/symbiotic-2ai53C/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "node_prepare_for_write" has inline asm
KLEE: WARNING ONCE: function "sm_disk_new_block" has inline asm
KLEE: WARNING ONCE: function "sm_ll_find_free_block" has inline asm
KLEE: WARNING ONCE: function "sm_ll_insert" has inline asm
KLEE: WARNING ONCE: function "dm_btree_remove" has inline asm
KLEE: WARNING ONCE: function "shadow_current" has inline asm
KLEE: WARNING ONCE: function "shadow_parent" has inline asm
KLEE: WARNING ONCE: function "bl_down_write" has inline asm
KLEE: WARNING ONCE: function "__check_holder" has inline asm
KLEE: WARNING ONCE: function "__add_holder" has inline asm
KLEE: WARNING ONCE: function "__wait" has inline asm
KLEE: WARNING ONCE: function "put_task_struct" has inline asm
KLEE: WARNING ONCE: function "__find_holder" has inline asm
KLEE: WARNING ONCE: function "dm_tm_inc" has inline asm
KLEE: WARNING ONCE: function "delete_at" has inline asm
KLEE: WARNING ONCE: function "dm_tm_dec" has inline asm
KLEE: WARNING ONCE: function "node_copy" has inline asm
KLEE: WARNING ONCE: function "node_shift" has inline asm
KLEE: WARNING ONCE: function "shift" has inline asm
KLEE: WARNING ONCE: function "dm_bm_read_try_lock" has inline asm
KLEE: WARNING ONCE: function "dm_bm_read_lock" has inline asm
KLEE: WARNING ONCE: function "bl_up_read" has inline asm
KLEE: WARNING ONCE: function "__wake_many" has inline asm
KLEE: WARNING ONCE: function "bl_up_write" has inline asm
KLEE: WARNING ONCE: function "sm_ll_lookup_bitmap" has inline asm
KLEE: WARNING ONCE: function "ro_node" has inline asm
KLEE: WARNING ONCE: function "shrink" has inline asm
KLEE: WARNING ONCE: function "fill_ablock" has inline asm
KLEE: WARNING ONCE: function "dm_btree_walk" has inline asm
KLEE: WARNING ONCE: function "ro_pop" has inline asm
KLEE: WARNING ONCE: function "dm_bitset_set_bit" has inline asm
KLEE: WARNING ONCE: function "dm_bitset_clear_bit" has inline asm
KLEE: WARNING ONCE: function "dm_bitset_test_bit" has inline asm
KLEE: WARNING ONCE: flushing 9592 bytes on read, may be slow and/or crash: MO58[9592] allocated at global:
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6224: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6144: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6144: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6204: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6204: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6145: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6239: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6205: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6164: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2ai53C/linux-3_false-termination.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c:6179: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
klee: /var/xchalup4/symbiotic/klee/lib/Core/SpecialFunctionHandler.cpp:250: std::__cxx11::string klee::SpecialFunctionHandler::readStringAtAddress(klee::ExecutionState&, klee::ref<klee::Expr>): Assertion `isa<ConstantExpr>(cur) && "hit symbolic char while reading concrete string"' failed.
0  klee            0x00000000012fcca8 llvm::sys::PrintStackTrace(llvm::raw_ostream&) + 56
1  klee            0x00000000012fac7e llvm::sys::RunSignalHandlers() + 62
2  klee            0x00000000012fadcc
3  libpthread.so.0 0x00007f51a96f2390
4  libc.so.6       0x00007f51a8aab428 gsignal + 56
5  libc.so.6       0x00007f51a8aad02a abort + 362
6  libc.so.6       0x00007f51a8aa3bd7
7  libc.so.6       0x00007f51a8aa3c82
8  klee            0x00000000005f7297 klee::SpecialFunctionHandler::readStringAtAddress[abi:cxx11](klee::ExecutionState&, klee::ref<klee::Expr>) + 1607
9  klee            0x00000000005f8ba7 klee::SpecialFunctionHandler::handleMakeSymbolic(klee::ExecutionState&, klee::KInstruction*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 183
10 klee            0x00000000005f6b9f klee::SpecialFunctionHandler::handle(klee::ExecutionState&, llvm::Function*, klee::KInstruction*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 143
11 klee            0x00000000005cdfa3 klee::Executor::callExternalFunction(klee::ExecutionState&, klee::KInstruction*, llvm::Function*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 83
12 klee            0x00000000005d3229 klee::Executor::executeCall(klee::ExecutionState&, klee::KInstruction*, llvm::Function*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 1321
13 klee            0x00000000005d8788 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 14952
14 klee            0x00000000005da8c5 klee::Executor::run(klee::ExecutionState&) + 2117
15 klee            0x00000000005daeef klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1391
16 klee            0x0000000000593c63 main + 8867
17 libc.so.6       0x00007f51a8a96830 __libc_start_main + 240
18 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 268.127029896
