bin/symbiotic --witness witness.graphml --no-slice --no-prepare --32 --prp=../sv-benchmarks/c/ReachSafety.prp ../sv-benchmarks/c/ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.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.: 34 96 2262 10861
INFO: Compilation, preparation and instrumentation time: 0.277597904205
Defining function KfAcquireSpinLock as symbolic
Defining function InterlockedExchange as symbolic
Defining function KeGetCurrentThread as symbolic
Defining function KeSetPriorityThread as symbolic
Removed calls to 'MmProbeAndLockPages' (function is undefined)
Linked our definitions to these undefined functions:
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_long_named
  __VERIFIER_nondet_pointer_named
INFO: After-slicing optimizations and preparation time: 0.2943379879
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 149 106 613 4821
INFO: Starting verification
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
klee: /var/xchalup4/symbiotic/klee/include/klee/Expr.h:1082: static klee::ref<klee::ConstantExpr> klee::ConstantExpr::create(uint64_t, klee::Expr::Width): Assertion `v == bits64::truncateToNBits(v, w) && "invalid constant"' failed.
KLEE: output directory is "/tmp/symbiotic-h42B2L/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
klee: /var/xchalup4/symbiotic/klee/include/klee/Expr.h:1082: static klee::ref<klee::ConstantExpr> klee::ConstantExpr::create(uint64_t, klee::Expr::Width): Assertion `v == bits64::truncateToNBits(v, w) && "invalid constant"' 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 0x00007f556eea0390
4  libc.so.6       0x00007f556e259428 gsignal + 56
5  libc.so.6       0x00007f556e25b02a abort + 362
6  libc.so.6       0x00007f556e251bd7
7  libc.so.6       0x00007f556e251c82
8  klee            0x0000000000606d3b klee::AddressSpace::resolve(klee::ExecutionState&, klee::TimingSolver*, klee::ref<klee::Expr>, std::vector<std::pair<klee::MemoryObject const*, klee::ObjectState const*>, std::allocator<std::pair<klee::MemoryObject const*, klee::ObjectState const*> > >&, unsigned int, double) + 4763
9  klee            0x00000000005d2610 klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool, klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 1456
10 klee            0x00000000005d598e klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 3182
11 klee            0x00000000005da8c5 klee::Executor::run(klee::ExecutionState&) + 2117
12 klee            0x00000000005daeef klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1391
13 klee            0x0000000000593c63 main + 8867
14 libc.so.6       0x00007f556e244830 __libc_start_main + 240
15 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 0.954900026321
