Closed rasoolmaghareh closed 1 year ago
Getting the following output for this program.
************Basic Block Coverage Report Starts****************
KLEE: done: Total number of single time Visited Basic Blocks: 16
KLEE: done: Total number of Basic Blocks: 16
************Basic Block Coverage Report Ends****************
************ICMP/Atomic Condition Coverage Report Starts****************
KLEE: done: Total number of Covered ICMP/Atomic Condition: 5
KLEE: done: Total number of All ICMP/Atomic Condition: 5
************ICMP/Atomic Condition Coverage Report Ends****************
KLEE: Memory cap NOT exceeded!
KLEE: done: Total reduced symbolic execution tree nodes = 87
KLEE: done: Total number of visited basic blocks = 521
KLEE: done: Subsumption statistics
KLEE: done: Time for actual solver calls in subsumption check (ms) = 5.368
KLEE: done: Number of solver calls for subsumption check (failed) = 5 (5)
KLEE: done: Concrete store expression build time (ms) = 19.887
KLEE: done: Symbolic store expression build time (ms) = 0.005
KLEE: done: Solver access time (ms) = 7.792
KLEE: done: Average table entries per subsumption checkpoint = 15.66
KLEE: done: Number of subsumption checks = 94
KLEE: done: Average solver calls per subsumption check = 0.05
KLEE: done: TxTree method execution times (ms):
KLEE: done: setCurrentINode = 0.747
KLEE: done: remove = 79.426
KLEE: done: subsumptionCheck = 647.769
KLEE: done: markPathCondition = 0.798
KLEE: done: split = 0.324
KLEE: done: executeOnNode = 1.612
KLEE: done: executeMemoryOperation = 4.673
KLEE: done: TxTreeNode method execution times (ms):
KLEE: done: getInterpolant = 0.214
KLEE: done: get WP Interpolant = 53.296
KLEE: done: addConstraintTime = 0.816
KLEE: done: splitTime = 0.244
KLEE: done: execute = 1.502
KLEE: done: bindCallArguments = 0
KLEE: done: bindReturnValue = 0
KLEE: done: getStoredExpressions = 0.18
KLEE: done: getStoredCoreExpressions = 0.478
KLEE: done: total instructions = 2327
KLEE: done: completed paths = 44, among which
KLEE: done: early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done: average branching depth of completed paths = 8.25
KLEE: done: average branching depth of subsumed paths = 6.4
KLEE: done: average instructions of completed paths = 465.25
KLEE: done: average instructions of subsumed paths = 333.925
KLEE: done: subsumed paths = 40
KLEE: done: error paths = 0
KLEE: done: program exit paths = 4
KLEE: done: generated tests = 0, among which
KLEE: done: early-terminating tests (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done: error tests = 0
KLEE: done: program exit tests = 0
KLEE: done: NOTE:
KLEE: done: Subsumed paths / tests counts are nondeterministic for
KLEE: done: programs with dynamically-allocated memory such as those
KLEE: done: using malloc, since KLEE may reuse the address of the
KLEE: done: same malloc calls in different paths. This nondeterminism
KLEE: done: does not cause loss of error reports.
-------------------------------------------------------------------------------------------
| Path | Instrs| Time(s)| ICov(%)| BCov(%)| ICount| TSolver(%)|
-------------------------------------------------------------------------------------------
|pointer_struct5-3/klee-out-0| 2327| 0.82| 23.39| 13.16| 342| 9.30|
-------------------------------------------------------------------------------------------
Thanks, closing this issue. Please also add which PR fixes this issue.
clang -emit-llvm -g -I/home/issta21-322/TracerX/tracerx/Release+Asserts/include -I/home/issta21-322/TracerX/tracerx/Release+Asserts/../include -Wno-int-conversion -c pointer_struct5.c SOLVER_FLAGS="-solver-backend=z3" OUTPUT_DIR=pointer_struct5.tx make pointer_struct5.klee-out make[1]: Entering directory '/home/issta21-322/TracerX-examples/basic' KLEE: output directory is "/home/issta21-322/TracerX-examples/basic/pointer_struct5.tx" Using Z3 solver backend KLEE: Logging all queries in .pc format to /home/issta21-322/TracerX-examples/basic/pointer_struct5.tx/all-queries.pc
KLEE: Logging all queries in .smt2 format to /home/issta21-322/TracerX-examples/basic/pointer_struct5.tx/all-queries.smt2
KLEE: Deterministic memory allocation starting from 0x7ff30000000 klee: TxWP.cpp:1193: klee::ref klee::TxWeakestPreCondition::getCallInst(llvm::CallInst): Assertion `ret && "Return instruction is null!"' failed.
0 klee 0x0000000000e983e2 llvm::sys::PrintStackTrace(_IO_FILE) + 50
1 klee 0x0000000000e97c34
2 libpthread.so.0 0x00007fd587d23390
3 libc.so.6 0x00007fd5854e0438 gsignal + 56
4 libc.so.6 0x00007fd5854e203a abort + 362
5 libc.so.6 0x00007fd5854d8be7
6 libc.so.6 0x00007fd5854d8c92
7 klee 0x00000000005dd326 klee::TxWeakestPreCondition::getCallInst(llvm::CallInst) + 294
8 klee 0x00000000005db8d5 klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value, klee::ref) + 933
9 klee 0x00000000005dcb27 klee::TxWeakestPreCondition::getCastInst(llvm::CastInst) + 87
10 klee 0x00000000005db873 klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value, klee::ref) + 835
11 klee 0x00000000005ddd10 klee::TxWeakestPreCondition::PushUp(std::vector<std::pair<klee::KInstruction, int>, std::allocator<std::pair<klee::KInstruction, int> > >) + 1296
12 klee 0x00000000005b7cd8 klee::TxTreeNode::generateWPInterpolant() + 1032
13 klee 0x00000000005be5eb klee::TxSubsumptionTableEntry::TxSubsumptionTableEntry(klee::TxTreeNode, std::vector<llvm::Instruction, std::allocator<llvm::Instruction> > const&) + 1163
14 klee 0x00000000005be96b klee::TxTree::remove(klee::ExecutionState, klee::TimingSolver, bool) + 779
15 klee 0x000000000054a3b1 klee::Executor::updateStates(klee::ExecutionState) + 513
16 klee 0x000000000056142e klee::Executor::run(klee::ExecutionState&) + 5982
17 klee 0x0000000000561f59 klee::Executor::runFunctionAsMain(llvm::Function*, int, char, char) + 1705
18 klee 0x000000000052825d main + 10365
19 libc.so.6 0x00007fd5854cb840 __libc_start_main + 240
20 klee 0x000000000053bb69 _start + 41
Command terminated by signal 6
0.07user 0.00system 0:00.30elapsed 26%CPU (0avgtext+0avgdata 26944maxresident)k
0inputs+232outputs (0major+1871minor)pagefaults 0swaps
make[2]: Entering directory '/home/issta21-322/TracerX-examples/basic'
warning: ignoring debug info with an invalid version (1) in pointer_struct5.bc
Writing 'cfg.main.dot'...
Printing analysis 'Print CFG of function to 'dot' file' for function 'main':
| Path | Instrs| Time(s)| ICov(%)| BCov(%)| ICount| TSolver(%)|
|pointer_struct5.tx| 0| 0.00| 0.00| 0.00| 342| 0.00|
make[2]: Leaving directory '/home/issta21-322/TracerX-examples/basic' make[1]: Leaving directory '/home/issta21-322/TracerX-examples/basic' grep: pointer_struct5.tx/tree.dot: No such file or directory ERROR: Subsumption number (0) disagrees with reference data for pointer_struct5.c (40) ../Makefile.common:120: recipe for target 'pointer_struct5.tx' failed make: *** [pointer_struct5.tx] Error 1