bin/symbiotic --witness witness.graphml --no-slice --no-prepare --32 --prp=../sv-benchmarks/c/ReachSafety.prp ../sv-benchmarks/c/ntdrivers/parport_true-unreach-call.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.: 63 181 2364 13258
INFO: Compilation, preparation and instrumentation time: 0.364202976227
Removed calls to 'IoAcquireCancelSpinLock' (function is undefined)
Removed calls to 'IoReleaseRemoveLockEx' (function is undefined)
Removed calls to 'IoReleaseRemoveLockAndWaitEx' (function is undefined)
Removed calls to 'IoWriteErrorLogEntry' (function is undefined)
Defining function IoAllocateErrorLogEntry as symbolic
Removed calls to 'IoDisconnectInterrupt' (function is undefined)
Removed calls to 'PoSetPowerState' (function is undefined)
Removed calls to 'IoInitializeRemoveLockEx' (function is undefined)
Removed calls to 'KeInitializeDpc' (function is undefined)
Removed calls to 'WRITE_PORT_UCHAR' (function is undefined)
Removed calls to 'KeStallExecutionProcessor' (function is undefined)
Defining function READ_PORT_UCHAR as symbolic
Removed calls to 'KeQueryTickCount' (function is undefined)
Defining function KeQueryTimeIncrement as symbolic
Defining function KeSynchronizeExecution as symbolic
Defining function RtlIntegerToUnicodeString as symbolic
Defining function RtlAppendUnicodeStringToString as symbolic
Defining function RtlUnicodeStringToInteger as symbolic
Defining function IoOpenDeviceRegistryKey as symbolic
Defining function ZwQueryValueKey as symbolic
Defining function PoRequestPowerIrp as symbolic
Defining function IoWMIRegistrationControl as symbolic
Removed calls to 'ObfReferenceObject' (function is undefined)
Defining function WmiCompleteRequest as symbolic
Defining function IoReportResourceUsage as symbolic
Defining function RtlCompareUnicodeString as symbolic
Defining function KeInsertQueueDpc as symbolic
Defining function IoConnectInterrupt as symbolic
Defining function InterlockedExchange as symbolic
Defining function InterlockedDecrement as symbolic
Defining function InterlockedIncrement as symbolic
Defining function ZwSetValueKey as symbolic
Linked our definitions to these undefined functions:
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_char_named
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_long_named
  __VERIFIER_nondet_pointer_named
INFO: After-slicing optimizations and preparation time: 0.418340206146
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 202 208 981 7371
INFO: Starting verification
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-aatDWH/klee-out-0"
KLEE: Using STP solver backend
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 0x00007f6981ea1390
4  libc.so.6       0x00007f698125a428 gsignal + 56
5  libc.so.6       0x00007f698125c02a abort + 362
6  libc.so.6       0x00007f6981252bd7
7  libc.so.6       0x00007f6981252c82
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       0x00007f6981245830 __libc_start_main + 240
15 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 1.38140296936
