rasoolmaghareh
commented
4 years ago Similar crash in klee-examples/basic/pointer_struct4.c
Closed rasoolmaghareh closed 11 months ago
rasoolmaghareh
commented
4 years ago Similar crash in klee-examples/basic/pointer_struct4.c
rasoolmaghareh
commented
4 years ago Similar crash in klee-examples/basic/pointer_struct5.c
rasoolmaghareh
commented
1 year ago This is the new output that I am seeing:
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_struct7.c
SOLVER_FLAGS="-solver-backend=z3" OUTPUT_DIR=pointer_struct7.tx make pointer_struct7.klee-out
make[1]: Entering directory '/home/issta21-322/TracerX-examples/basic'
KLEE: output directory is "/home/issta21-322/TracerX-examples/basic/pointer_struct7.tx"
Using Z3 solver backend
KLEE: Logging all queries in .pc format to /home/issta21-322/TracerX-examples/basic/pointer_struct7.tx/all-queries.pc
KLEE: Logging all queries in .smt2 format to /home/issta21-322/TracerX-examples/basic/pointer_struct7.tx/all-queries.smt2
KLEE: Deterministic memory allocation starting from 0x7ff30000000
klee: TxWP.cpp:1193: klee::ref<klee::Expr> 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 0x00007fe999d94390
3 libc.so.6 0x00007fe997551438 gsignal + 56
4 libc.so.6 0x00007fe99755303a abort + 362
5 libc.so.6 0x00007fe997549be7
6 libc.so.6 0x00007fe997549c92
7 klee 0x00000000005dd326 klee::TxWeakestPreCondition::getCallInst(llvm::CallInst*) + 294
8 klee 0x00000000005db8d5 klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value*, klee::ref<klee::Expr>) + 933
9 klee 0x00000000005dcb27 klee::TxWeakestPreCondition::getCastInst(llvm::CastInst*) + 87
10 klee 0x00000000005db873 klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value*, klee::ref<klee::Expr>) + 835
11 klee 0x00000000005ddd10 klee::TxWeakestPreCondition::PushUp(std::vector<std::pair<klee::KInstruction*, int>, std::allocator<std::pair<klee::KInstruction*, int> > >) + 1296
12 klee 0x00000000005b7bea klee::TxTreeNode::generateWPInterpolant() + 794
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 0x00007fe99753c840 __libc_start_main + 240
20 klee 0x000000000053bb69 _start + 41
Command terminated by signal 6
0.04user 0.00system 0:00.29elapsed 19%CPU (0avgtext+0avgdata 26080maxresident)k
0inputs+224outputs (0major+1567minor)pagefaults 0swaps
make[2]: Entering directory '/home/issta21-322/TracerX-examples/basic'
warning: ignoring debug info with an invalid version (1) in pointer_struct7.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_struct7.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'
ArpitaDutta
commented
1 year ago Unable to return the callInst to TxWeakestPreCondition::generateExprFromOperand()
for the following instruction
%17 = call noalias i8* @malloc(i64 16) #7, !dbg !139
Is it because this instruction is calling the malloc function and their is no return from this function?
Following is the whole body for malloc function is only this much. malloc returns a pointer but their is no explicit return statement.
; Function Attrs: nounwind
declare noalias i8* @malloc(i64) #3I think we need to handle this as a special case.
rasoolmaghareh
commented
1 year ago Maybe we need to discuss the meaning of the WP push up in this scenario. Can you please print the C instruction as well as the WP expression reaching this point?
ArpitaDutta
commented
1 year ago Here is debug subsumption log along with the instructions for pushup functions.
In the last few lines before the crash messages, I have printed the instructions involved in the operation of store which are ultimately resulting into this state.
KLEE: Subsumption check for Node #1, Program Point 61603864
KLEE: #1: Check failure due to control point not found in table
KLEE: Subsumption check for Node #2, Program Point 61606552
KLEE: #2: Check failure due to control point not found in table
KLEE: Subsumption check for Node #3, Program Point 61606552
KLEE: #3: Check failure due to control point not found in table
KLEE: Subsumption check for Node #4, Program Point 61606552
KLEE: #4: Check failure due to control point not found in table
KLEE: Subsumption check for Node #5, Program Point 61606552
KLEE: #5: Check failure due to control point not found in table
KLEE: Subsumption check for Node #6, Program Point 61606552
KLEE: #6: Check failure due to control point not found in table
KLEE: Subsumption check for Node #7, Program Point 61606552
KLEE: #7: Check failure due to control point not found in table
KLEE: Subsumption check for Node #8, Program Point 61606552
KLEE: #8: Check failure due to control point not found in table
KLEE: Subsumption check for Node #9, Program Point 61606552
KLEE: #9: Check failure due to control point not found in table
KLEE: Storing entry for Node #9, Program Point 61606552
Current Pushup Instruction: ret i32 %57, !dbg !152
Current Pushup Instruction: %57 = load i32* %z, align 4, !dbg !152
Current Pushup Instruction: br label %56, !dbg !151
Current Pushup Instruction: br i1 %52, label %53, label %54, !dbg !151
Current Pushup Instruction: %52 = icmp slt i32 %49, %51, !dbg !151
Current Pushup Instruction: %51 = add nsw i32 %50, 999, !dbg !151
Current Pushup Instruction: %50 = load i32* @n, align 4, !dbg !151
Current Pushup Instruction: %49 = load i32* %48, align 4, !dbg !151
Current Pushup Instruction: %48 = getelementptr inbounds %struct.node* %47, i32 0, i32 0, !dbg !151
Current Pushup Instruction: %47 = load %struct.node** %x, align 8, !dbg !151
Current Pushup Instruction: br i1 %15, label %16, label %46, !dbg !135
Current Pushup Instruction: %15 = icmp slt i32 %14, 9, !dbg !135
Current Pushup Instruction: %14 = load i32* %i, align 4, !dbg !135
Current Pushup Instruction: br label %13, !dbg !135
Current Pushup Instruction: store i32 %45, i32* %i, align 4, !dbg !135
Current Pushup Instruction: %45 = add nsw i32 %44, 1, !dbg !135
Current Pushup Instruction: %44 = load i32* %i, align 4, !dbg !135
Current Pushup Instruction: br label %43, !dbg !150
Current Pushup Instruction: store %struct.node* %42, %struct.node** %x, align 8, !dbg !149
Current Pushup Instruction: %42 = load %struct.node** %y, align 8, !dbg !149
Current Pushup Instruction: br label %41
Current Pushup Instruction: store i32 %38, i32* %40, align 4, !dbg !148
Current Pushup Instruction: %40 = getelementptr inbounds %struct.node* %39, i32 0, i32 0, !dbg !148
Current Pushup Instruction: %39 = load %struct.node** %y, align 8, !dbg !148
Current Pushup Instruction: %38 = add nsw i32 %37, 10, !dbg !148
Current Pushup Instruction: %37 = load i32* %36, align 4, !dbg !148
Current Pushup Instruction: %36 = getelementptr inbounds %struct.node* %35, i32 0, i32 0, !dbg !148
Current Pushup Instruction: %35 = load %struct.node** %x, align 8, !dbg !148
Current Pushup Instruction: store i32 %34, i32* %z, align 4, !dbg !146
Current Pushup Instruction: %34 = add nsw i32 %33, 2, !dbg !146
Current Pushup Instruction: %33 = load i32* %z, align 4, !dbg !146
KLEE: ------------ Subsumption Table Entry ------------
Program point = 61606552
C-File Name:Function Name:Line number = pointer_struct7.c:main:43
global = []
pi = (Sle (ReadLSB w32 0 __shadow__n)
0)
concretely-addressed store = [
address:
function/value: main/ %x = alloca %struct.node*, align 8
stack: (empty)
offset: 0
content:
function/value: main/ %42 = load %struct.node** %y, align 8, !dbg !149
OFFSETS:
[[base: 61492736, size: 16]=={0}]
reason(s) for storage:
branch infeasibility [main: Line 50]
pointer use [main: Line 38]
pointer use [main: Line 44]
------------------------------------------
address:
function/value: @n = common global i32 0, align 4
stack: (empty)
offset: 0
content:
function/value: main/ %4 = load i32* @n, align 4, !dbg !132
(ReadLSB w32 0 __shadow__n)
reason(s) for storage:
branch infeasibility [main: Line 50]
------------------------------------------
address:
function/value: main/ %17 = call noalias i8* @malloc(i64 16) #7, !dbg !139
stack: (empty)
offset: 0
content:
function/value: main/ %38 = add nsw i32 %37, 10, !dbg !148
(Add w32 70
(ReadLSB w32 0 __shadow__n))
reason(s) for storage:
branch infeasibility [main: Line 50]
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__n]
wp interpolant = [(Sle 8 (WPVar w32 (i)))]
KLEE: Subsumption check for Node #10, Program Point 61605992
KLEE: #10: Check failure due to control point not found in table
KLEE: Storing entry for Node #10, Program Point 61605992
Current Pushup Instruction: ret i32 %57, !dbg !152
Current Pushup Instruction: %57 = load i32* %z, align 4, !dbg !152
Current Pushup Instruction: br label %56, !dbg !151
Current Pushup Instruction: br i1 %52, label %53, label %54, !dbg !151
Current Pushup Instruction: %52 = icmp slt i32 %49, %51, !dbg !151
Current Pushup Instruction: %51 = add nsw i32 %50, 999, !dbg !151
Current Pushup Instruction: %50 = load i32* @n, align 4, !dbg !151
Current Pushup Instruction: %49 = load i32* %48, align 4, !dbg !151
Current Pushup Instruction: %48 = getelementptr inbounds %struct.node* %47, i32 0, i32 0, !dbg !151
Current Pushup Instruction: %47 = load %struct.node** %x, align 8, !dbg !151
Current Pushup Instruction: br i1 %15, label %16, label %46, !dbg !135
Current Pushup Instruction: %15 = icmp slt i32 %14, 9, !dbg !135
Current Pushup Instruction: %14 = load i32* %i, align 4, !dbg !135
Current Pushup Instruction: br label %13, !dbg !135
Current Pushup Instruction: store i32 %45, i32* %i, align 4, !dbg !135
Current Pushup Instruction: %45 = add nsw i32 %44, 1, !dbg !135
Current Pushup Instruction: %44 = load i32* %i, align 4, !dbg !135
Current Pushup Instruction: br label %43, !dbg !150
Current Pushup Instruction: store %struct.node* %42, %struct.node** %x, align 8, !dbg !149
Current Pushup Instruction: %42 = load %struct.node** %y, align 8, !dbg !149
Current Pushup Instruction: br label %41, !dbg !145
Current Pushup Instruction: store i32 %29, i32* %31, align 4, !dbg !144
Current Pushup Instruction: %31 = getelementptr inbounds %struct.node* %30, i32 0, i32 0, !dbg !144
Current Pushup Instruction: %30 = load %struct.node** %y, align 8, !dbg !144
Current Pushup Instruction: %29 = add nsw i32 %28, 10, !dbg !144
Current Pushup Instruction: %28 = load i32* %27, align 4, !dbg !144
Current Pushup Instruction: %27 = getelementptr inbounds %struct.node* %26, i32 0, i32 0, !dbg !144
Current Pushup Instruction: %26 = load %struct.node** %x, align 8, !dbg !144
Current Pushup Instruction: store i32 %25, i32* %z, align 4, !dbg !142
Current Pushup Instruction: %25 = add nsw i32 %24, 1, !dbg !142
Current Pushup Instruction: %24 = load i32* %z, align 4, !dbg !142
KLEE: ------------ Subsumption Table Entry ------------
Program point = 61605992
C-File Name:Function Name:Line number = pointer_struct7.c:main:40
global = []
pi = (Sle (ReadLSB w32 0 __shadow__n)
0)
concretely-addressed store = [
address:
function/value: main/ %x = alloca %struct.node*, align 8
stack: (empty)
offset: 0
content:
function/value: main/ %42 = load %struct.node** %y, align 8, !dbg !149
OFFSETS:
[[base: 61492736, size: 16]=={0}]
reason(s) for storage:
branch infeasibility [main: Line 50]
pointer use [main: Line 38]
pointer use [main: Line 41]
------------------------------------------
address:
function/value: @n = common global i32 0, align 4
stack: (empty)
offset: 0
content:
function/value: main/ %4 = load i32* @n, align 4, !dbg !132
(ReadLSB w32 0 __shadow__n)
reason(s) for storage:
branch infeasibility [main: Line 50]
------------------------------------------
address:
function/value: main/ %17 = call noalias i8* @malloc(i64 16) #7, !dbg !139
stack: (empty)
offset: 0
content:
function/value: main/ %38 = add nsw i32 %37, 10, !dbg !148
(Add w32 70
(ReadLSB w32 0 __shadow__n))
reason(s) for storage:
branch infeasibility [main: Line 50]
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__n]
wp interpolant = [(Sle 8 (WPVar w32 (i)))]
KLEE: Storing entry for Node #8, Program Point 51669656
Current Pushup Instruction: br i1 %22, label %23, label %32, !dbg !140
Current Pushup Instruction: %22 = icmp ne i8 %21, 0, !dbg !140
Current Pushup Instruction: %21 = load i8* %nondet, align 1, !dbg !140
Current Pushup Instruction: store %struct.node* %18, %struct.node** %20, align 8, !dbg !139
Current Pushup Instruction: %20 = getelementptr inbounds %struct.node* %19, i32 0, i32 1, !dbg !139
Current Pushup Instruction: %19 = load %struct.node** %x, align 8, !dbg !139
Current Pushup Instruction: store %struct.node* %18, %struct.node** %y, align 8, !dbg !139
****** Flag = 3 *******
store %struct.node* %18, %struct.node** %y, align 8, !dbg !139
------
No of operands: 2
getOperand(0) ==> %18 = bitcast i8* %17 to %struct.node*, !dbg !139
getOperand(0) type ==> %struct.node*
getOperand(1) ==> %y = alloca %struct.node*, align 8
getOperand(1) type ==> %struct.node**
****** Flag = 4 *******
store %struct.node* %18, %struct.node** %y, align 8, !dbg !139
------
Cp1
%18 = bitcast i8* %17 to %struct.node*, !dbg !139
Cp1
%17 = call noalias i8* @malloc(i64 16) #7, !dbg !139
Cp9
klee: TxWP.cpp:1286: klee::ref<klee::Expr> klee::TxWeakestPreCondition::getCallInst(llvm::CallInst*): Assertion `ret && "Return instruction is null!"' failed.
0 klee 0x0000000000ea14f2 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1 klee 0x0000000000ea0d44
2 libpthread.so.0 0x00007f797c118390
3 libc.so.6 0x00007f7979897438 gsignal + 56
4 libc.so.6 0x00007f797989903a abort + 362
5 libc.so.6 0x00007f797988fbe7
6 libc.so.6 0x00007f797988fc92
7 klee 0x00000000005e5676 klee::TxWeakestPreCondition::getCallInst(llvm::CallInst*) + 294
8 klee 0x00000000005e3bdb klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value*, klee::ref<klee::Expr>) + 1387
9 klee 0x00000000005e4e77 klee::TxWeakestPreCondition::getCastInst(llvm::CastInst*) + 87
10 klee 0x00000000005e3b13 klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value*, klee::ref<klee::Expr>) + 1187
11 klee 0x00000000005e6095 klee::TxWeakestPreCondition::PushUp(std::vector<std::pair<klee::KInstruction*, int>, std::allocator<std::pair<klee::KInstruction*, int> > >) + 1349
12 klee 0x00000000005bf4ea klee::TxTreeNode::generateWPInterpolant() + 794
13 klee 0x00000000005c6a9b klee::TxSubsumptionTableEntry::TxSubsumptionTableEntry(klee::TxTreeNode*, std::vector<llvm::Instruction*, std::allocator<llvm::Instruction*> > const&) + 1051
14 klee 0x00000000005c6c1c klee::TxTree::remove(klee::ExecutionState*, klee::TimingSolver*, bool) + 300
15 klee 0x00000000005542d1 klee::Executor::updateStates(klee::ExecutionState*) + 513
16 klee 0x00000000005691ce klee::Executor::run(klee::ExecutionState&) + 6222
17 klee 0x0000000000569e7a klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1850
18 klee 0x000000000052f71d main + 12941
19 libc.so.6 0x00007f7979882840 __libc_start_main + 240
20 klee 0x0000000000543089 _start + 41
KLEE: WARNING: KLEE: watchdog exiting (no child)Need to check the formulation more, maybe we can switch to deletion interpolation for this case if it is too hard to support.
ArpitaDutta
commented
1 year ago Fixed the crash by switching to deletion interpolation when the return from the call instruction is null. (Commit 7672a88a54253578375ea9facb2e990e86922c4c)
ArpitaDutta
commented
1 year ago WP Output:
************Basic Block Coverage Report Starts****************
KLEE: done: Total number of single time Visited Basic Blocks: 10
KLEE: done: Total number of Basic Blocks: 12
************Basic Block Coverage Report Ends****************
************ICMP/Atomic Condition Coverage Report Starts****************
KLEE: done: Total number of Covered ICMP/Atomic Condition: 4
KLEE: done: Total number of All ICMP/Atomic Condition: 4
************ICMP/Atomic Condition Coverage Report Ends****************
KLEE: Memory cap NOT exceeded!
KLEE: done: Total reduced symbolic execution tree nodes = 31
KLEE: done: Total number of visited basic blocks = 101
KLEE: done: Subsumption statistics
KLEE: done: Time for actual solver calls in subsumption check (ms) = 0
KLEE: done: Number of solver calls for subsumption check (failed) = 0 (0)
KLEE: done: Concrete store expression build time (ms) = 7.188
KLEE: done: Symbolic store expression build time (ms) = 0.004
KLEE: done: Solver access time (ms) = 3.45
KLEE: done: Average table entries per subsumption checkpoint = 5.66
KLEE: done: Number of subsumption checks = 31
KLEE: done: Average solver calls per subsumption check = 0.00
KLEE: done: TxTree method execution times (ms):
KLEE: done: setCurrentINode = 0.633
KLEE: done: remove = 50.818
KLEE: done: subsumptionCheck = 13.154
KLEE: done: markPathCondition = 0.28
KLEE: done: split = 0.372
KLEE: done: executeOnNode = 0.975
KLEE: done: executeMemoryOperation = 8.007
KLEE: done: TxTreeNode method execution times (ms):
KLEE: done: getInterpolant = 0.257
KLEE: done: get WP Interpolant = 36.065
KLEE: done: addConstraintTime = 0.615
KLEE: done: splitTime = 0.298
KLEE: done: execute = 0.881
KLEE: done: bindCallArguments = 0
KLEE: done: bindReturnValue = 0
KLEE: done: getStoredExpressions = 0.124
KLEE: done: getStoredCoreExpressions = 0.574
KLEE: done: total instructions = 535
KLEE: done: completed paths = 16, 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
KLEE: done: average branching depth of subsumed paths = 5
KLEE: done: average instructions of completed paths = 278.5
KLEE: done: average instructions of subsumed paths = 159.5
KLEE: done: subsumed paths = 14
KLEE: done: error paths = 0
KLEE: done: program exit paths = 2
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_struct7-3/klee-out-0| 535| 0.14| 22.81| 6.94| 342| 28.17|
-------------------------------------------------------------------------------------------Deletion Output:
************Basic Block Coverage Report Starts****************
KLEE: done: Total number of single time Visited Basic Blocks: 10
KLEE: done: Total number of Basic Blocks: 12
************Basic Block Coverage Report Ends****************
************ICMP/Atomic Condition Coverage Report Starts****************
KLEE: done: Total number of Covered ICMP/Atomic Condition: 4
KLEE: done: Total number of All ICMP/Atomic Condition: 4
************ICMP/Atomic Condition Coverage Report Ends****************
KLEE: Memory cap NOT exceeded!
KLEE: done: Total reduced symbolic execution tree nodes = 31
KLEE: done: Total number of visited basic blocks = 101
KLEE: done: Subsumption statistics
KLEE: done: Time for actual solver calls in subsumption check (ms) = 0
KLEE: done: Number of solver calls for subsumption check (failed) = 0 (0)
KLEE: done: Concrete store expression build time (ms) = 10.258
KLEE: done: Symbolic store expression build time (ms) = 0.005
KLEE: done: Solver access time (ms) = 4.289
KLEE: done: Average table entries per subsumption checkpoint = 5.66
KLEE: done: Number of subsumption checks = 31
KLEE: done: Average solver calls per subsumption check = 0.00
KLEE: done: TxTree method execution times (ms):
KLEE: done: setCurrentINode = 0.672
KLEE: done: remove = 17.367
KLEE: done: subsumptionCheck = 17.225
KLEE: done: markPathCondition = 0.298
KLEE: done: split = 0.421
KLEE: done: executeOnNode = 1.048
KLEE: done: executeMemoryOperation = 8.016
KLEE: done: TxTreeNode method execution times (ms):
KLEE: done: getInterpolant = 0.285
KLEE: done: addConstraintTime = 0.666
KLEE: done: splitTime = 0.305
KLEE: done: execute = 0.957
KLEE: done: bindCallArguments = 0
KLEE: done: bindReturnValue = 0
KLEE: done: getStoredExpressions = 0.174
KLEE: done: getStoredCoreExpressions = 0.682
KLEE: done: total instructions = 535
KLEE: done: completed paths = 16, 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
KLEE: done: average branching depth of subsumed paths = 5
KLEE: done: average instructions of completed paths = 278.5
KLEE: done: average instructions of subsumed paths = 159.5
KLEE: done: subsumed paths = 14
KLEE: done: error paths = 0
KLEE: done: program exit paths = 2
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_struct7-2/klee-out-0| 535| 0.11| 22.81| 6.94| 342| 30.07|
-------------------------------------------------------------------------------------------Thanks @ArpitaDutta. Closing this issue.
Crash in
TxWeakestPreCondition::getCallInst: