Crash on klee-examples/basic/arraysimple5.c with WP

[rasoolmaghareh]

Crash in TxTreeNode::instantiateWPatSubsumption:

KLEE: Logging all queries in .smt2 format to /home/sajjad/Tracer-X/klee-examples/basic/arraysimple5.tx/all-queries.smt2

KLEE: Deterministic memory allocation starting from 0x7ff30000000
klee: TxTree.cpp:2956: klee::ref<klee::Expr> klee::TxTreeNode::instantiateWPatSubsumption(klee::ref<klee::Expr>, klee::TxDependency*): Assertion `isa<ConstantExpr>(offset) && "TxTreeNode::" "instantiateWPatSubsumption, offset is " "not a constant value"' failed.
0  libLLVM-3.4.so  0x00007fbda8929052 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1  libLLVM-3.4.so  0x00007fbda89287c4
2  libpthread.so.0 0x00007fbda8026390
3  libc.so.6       0x00007fbda59c4428 gsignal + 56
4  libc.so.6       0x00007fbda59c602a abort + 362
5  libc.so.6       0x00007fbda59bcbd7
6  libc.so.6       0x00007fbda59bcc82
7  klee            0x00000000004ef7a5 klee::TxTreeNode::instantiateWPatSubsumption(klee::ref<klee::Expr>, klee::TxDependency*) + 2741
8  klee            0x00000000004eef9c klee::TxTreeNode::instantiateWPatSubsumption(klee::ref<klee::Expr>, klee::TxDependency*) + 684
9  klee            0x00000000004f1402 klee::TxSubsumptionTableEntry::subsumed(klee::TimingSolver*, klee::ExecutionState&, double, bool, std::map<klee::ref<klee::TxAllocationContext>, klee::TxStore::MiddleStateStore, std::less<klee::ref<klee::TxAllocationContext> >, std::allocator<std::pair<klee::ref<klee::TxAllocationContext> const, klee::TxStore::MiddleStateStore> > >&, std::map<klee::ref<klee::TxVariable>, klee::ref<klee::TxStoreEntry>, std::less<klee::ref<klee::TxVariable> >, std::allocator<std::pair<klee::ref<klee::TxVariable> const, klee::ref<klee::TxStoreEntry> > > >&, std::map<klee::ref<klee::TxVariable>, klee::ref<klee::TxStoreEntry>, std::less<klee::ref<klee::TxVariable> >, std::allocator<std::pair<klee::ref<klee::TxVariable> const, klee::ref<klee::TxStoreEntry> > > >&, int) + 1298
10 klee            0x00000000004f5603 klee::TxSubsumptionTable::check(klee::TimingSolver*, klee::ExecutionState&, double, int) + 851
11 klee            0x00000000004f58ff klee::TxTree::subsumptionCheck(klee::TimingSolver*, klee::ExecutionState&, double) + 223
12 klee            0x0000000000494634 klee::Executor::run(klee::ExecutionState&) + 6436
13 klee            0x0000000000494fd6 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1686
14 klee            0x000000000046560d main + 12765
15 libc.so.6       0x00007fbda59af830 __libc_start_main + 240
16 klee            0x000000000046e0c9 _start + 41
Command terminated by signal 6
0.03user 0.00system 0:00.34elapsed 11%CPU (0avgtext+0avgdata 33280maxresident)k
0inputs+248outputs (0major+1593minor)pagefaults 0swaps

[rasoolmaghareh]

Similar crash in /klee-examples/basic/bubble_assert.c

[xuanlinhha]

Hi @rasoolmaghareh , in the arraysimple5.c, when creating a concrete value for this expr:

(Eq 97
     (Sel w32 (WPVar w32 (a))
              (ZExt w64 (WPVar w32 (i)))))

The WPVar(i) is a symbolic value (ReadLSB w32 0 i) in the dependency, so how should we deal with this case?

[xuanlinhha]

The pi is null at this point, but the check failed inside this function TxTreeNode::instantiateWPatSubsumption. You don't allow the index of Sel expression is a symbolic value. I think if we allow index is symbolic, then the returned value will be a Sel expr with symbolic index but currently, we don't have code for checking such type of expression in z3, don't support for conversion of that type of expr to z3

[rasoolmaghareh]

I see, can we return the expression with symbolic sel and then fail the subsumption check in the TxSubsumptionTableEntry::subsumed function? Later we will write a code to convert this to Z3 expression.

[xuanlinhha]

@rasoolmaghareh In the case that index is symbolic I return a nil value so that the checking is failed.

[rasoolmaghareh]

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 arraysimple5.c
SOLVER_FLAGS="-solver-backend=z3" OUTPUT_DIR=arraysimple5.tx make arraysimple5.klee-out
make[1]: Entering directory '/home/issta21-322/TracerX-examples/basic'
KLEE: output directory is "/home/issta21-322/TracerX-examples/basic/arraysimple5.tx"
Using Z3 solver backend
KLEE: Logging all queries in .pc format to /home/issta21-322/TracerX-examples/basic/arraysimple5.tx/all-queries.pc

KLEE: Logging all queries in .smt2 format to /home/issta21-322/TracerX-examples/basic/arraysimple5.tx/all-queries.smt2

KLEE: Deterministic memory allocation starting from 0x7ff30000000
klee: TxTree.cpp:3113: klee::ref<klee::Expr> klee::TxTreeNode::instantiateWPatSubsumption(klee::ref<klee::Expr>, klee::ExecutionState&, klee::TxDependency*): Assertion `isa<ConstantExpr>(offset) && "TxTreeNode::" "instantiateWPatSubsumption, offset is " "not a constant value"' failed.
0  klee            0x0000000000e983e2 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1  klee            0x0000000000e97c34
2  libpthread.so.0 0x00007f05d7227390
3  libc.so.6       0x00007f05d49e4438 gsignal + 56
4  libc.so.6       0x00007f05d49e603a abort + 362
5  libc.so.6       0x00007f05d49dcbe7
6  libc.so.6       0x00007f05d49dcc92
7  klee            0x00000000005bddff klee::TxTreeNode::instantiateWPatSubsumption(klee::ref<klee::Expr>, klee::ExecutionState&, klee::TxDependency*) + 4559
8  klee            0x00000000005bcf4a klee::TxTreeNode::instantiateWPatSubsumption(klee::ref<klee::Expr>, klee::ExecutionState&, klee::TxDependency*) + 794
9  klee            0x00000000005bf876 klee::TxSubsumptionTableEntry::subsumed(klee::TimingSolver*, klee::ExecutionState&, double, bool, std::map<klee::ref<klee::TxAllocationContext>, klee::TxStore::MiddleStateStore, std::less<klee::ref<klee::TxAllocationContext> >, std::allocator<std::pair<klee::ref<klee::TxAllocationContext> const, klee::TxStore::MiddleStateStore> > >&, std::map<klee::ref<klee::TxVariable>, klee::ref<klee::TxStoreEntry>, std::less<klee::ref<klee::TxVariable> >, std::allocator<std::pair<klee::ref<klee::TxVariable> const, klee::ref<klee::TxStoreEntry> > > >&, std::map<klee::ref<klee::TxVariable>, klee::ref<klee::TxStoreEntry>, std::less<klee::ref<klee::TxVariable> >, std::allocator<std::pair<klee::ref<klee::TxVariable> const, klee::ref<klee::TxStoreEntry> > > >&, int) + 966
10 klee            0x00000000005c3c0b klee::TxSubsumptionTable::check(klee::TimingSolver*, klee::ExecutionState&, double, int) + 859
11 klee            0x00000000005c3eff klee::TxTree::subsumptionCheck(klee::TimingSolver*, klee::ExecutionState&, double) + 223
12 klee            0x00000000005616c5 klee::Executor::run(klee::ExecutionState&) + 6645
13 klee            0x0000000000561f59 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1705
14 klee            0x000000000052825d main + 10365
15 libc.so.6       0x00007f05d49cf840 __libc_start_main + 240
16 klee            0x000000000053bb69 _start + 41
Command terminated by signal 6
0.05user 0.01system 0:00.35elapsed 18%CPU (0avgtext+0avgdata 26388maxresident)k
0inputs+248outputs (0major+1728minor)pagefaults 0swaps
make[2]: Entering directory '/home/issta21-322/TracerX-examples/basic'
warning: ignoring debug info with an invalid version (1) in arraysimple5.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(%)|
------------------------------------------------------------------------------
|arraysimple5.tx|       0|     0.00|     0.00|     0.00|     366|        0.00|
------------------------------------------------------------------------------
make[2]: Leaving directory '/home/issta21-322/TracerX-examples/basic'
make[1]: Leaving directory '/home/issta21-322/TracerX-examples/basic'

[ArpitaDutta]

Still we are facing this crash due to the WPVar(i) which is a symbolic variable (ReadLSB w32 0 i). In the sel expr (Sel w32 (WPVar w32 (a)) (ZExt w64 (WPVar w32 (i))), we have checks to find to whether the index variable is a constant expression or not. Even if we remove those checks, we will face issue in some point.

Is it okay (for the time being) if we return dummy from TxTreeNode::instantiateWPatSubsumption() whenever Sel index is symbolic and continue the execution?

[rasoolmaghareh]

It seems that the issue should be related to the ZExt expression part which is increasing the index variable size form 32 bits to 64 by adding 0 before it. Do we support (ZExt w64 (WPVar w32 (i)) in the instantiateWPatSubsumption() function?

[ArpitaDutta]

Yes, we support ZExt in instantiateWPatSubsumption(). The return of this case is (ZExt w64 (ReadLSB w32 0 i))

[rasoolmaghareh]

I think it's fine to return dummy for now, but we need to keep this issue open to revisit this issue and see why we are getting symbolic index in the expression.

[ArpitaDutta]

Sure.

[rasoolmaghareh]

This is something that we don't see in real programs very often: symbolic array index hence it does not have a high priority for us to address at the current point. We need to print a warning message too.

[ArpitaDutta]

Fixed this issue by skipping the instantiation for the symbolic array index or any non-constant array index. (Commit c4ca337)

However, there is a difference in the number of instructions executed by the deletion and WP branches. WP is taking more number of instructions than Deletion.

Logs for both branches are as follows:

Deletion log:

KLEE: KLEE: WATCHDOG: watching 8051

KLEE: output directory is "/home/arpita/Documents/TracerX-Work/crashes/klee-out-0"
Using Z3 solver backend
KLEE: Subsumption check for Node #1, Program Point 47398936
KLEE: #1: Check failure due to control point not found in table
KLEE: Subsumption check for Node #2, Program Point 47401512
KLEE: #2: Check failure due to control point not found in table
KLEE: Subsumption check for Node #3, Program Point 47401960
KLEE: #3: Check failure due to control point not found in table
KLEE: Subsumption check for Node #4, Program Point 47402744
KLEE: #4: Check failure due to control point not found in table
KLEE: Subsumption check for Node #5, Program Point 47403976
KLEE: #5: Check failure due to control point not found in table
KLEE: Subsumption check for Node #6, Program Point 47404424
KLEE: #6: Check failure due to control point not found in table
KLEE: Subsumption check for Node #7, Program Point 47405432
KLEE: #7: Check failure due to control point not found in table
KLEE: Storing entry for Node #7, Program Point 47405432
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47405432
C-File Name:Function Name:Line number = arraysimple5.c:main:70
global = []
pi = (empty)
concretely-addressed store = []
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = []
KLEE: Subsumption check for Node #8, Program Point 47404648
KLEE: #8: Check failure due to control point not found in table
KLEE: Storing entry for Node #8, Program Point 47404648
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47404648
C-File Name:Function Name:Line number = arraysimple5.c:main:66
global = []
pi = (And (Ult N0:(ReadLSB w32 0 __shadow__i)
           4)
      (Ult N0 2))
concretely-addressed store = []
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
KLEE: Storing entry for Node #6, Program Point 47404424
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47404424
C-File Name:Function Name:Line number = :main:0
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = []
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
KLEE: Subsumption check for Node #9, Program Point 47404088
KLEE: #9: Check failure due to control point not found in table
KLEE: Subsumption check for Node #10, Program Point 47405432
KLEE: #10=>#7: Global check success
KLEE: #10=>#7: Check success due to empty table entry
KLEE: Subsumption check for Node #11, Program Point 47404648
KLEE: #11=>#8: Global check success
KLEE: Before simplification:

KLEE: Existentials not empty
KLEE: Querying for subsumption check:

KLEE: #11=>#8: Check success as solver decided validity
KLEE: Storing entry for Node #9, Program Point 47404088
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47404088
C-File Name:Function Name:Line number = arraysimple5.c:main:59
global = []
pi = (empty)
concretely-addressed store = []
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = []
KLEE: Storing entry for Node #5, Program Point 47403976
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47403976
C-File Name:Function Name:Line number = arraysimple5.c:main:58
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = []
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
KLEE: Subsumption check for Node #12, Program Point 47403416
KLEE: #12: Check failure due to control point not found in table
KLEE: Subsumption check for Node #13, Program Point 47403864
KLEE: #13: Check failure due to control point not found in table
KLEE: Storing entry for Node #13, Program Point 47403864
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47403864
C-File Name:Function Name:Line number = arraysimple5.c:main:57
global = []
pi = (And (Ult N0:(ReadLSB w32 0 __shadow__i)
           4)
      (Eq false (Ult 1 N0)))
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
KLEE: Subsumption check for Node #14, Program Point 47403528
KLEE: #14: Check failure due to control point not found in table
KLEE: Storing entry for Node #14, Program Point 47403528
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47403528
C-File Name:Function Name:Line number = arraysimple5.c:main:56
global = []
pi = (Ult 1
      (ReadLSB w32 0 __shadow__i))
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
KLEE: Storing entry for Node #12, Program Point 47403416
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47403416
C-File Name:Function Name:Line number = arraysimple5.c:main:55
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
KLEE: Storing entry for Node #4, Program Point 47402744
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47402744
C-File Name:Function Name:Line number = arraysimple5.c:main:50
global = []
pi = (And (Ult (ReadLSB w32 0 __shadow__i)
           4)
      (Eq false
          (Ult 2
               (ReadLSB w32 0 __shadow__j))))
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
        ------------------------------------------
        address:
                function/value name: main/  %j = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__j)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i, __shadow__j]
KLEE: Subsumption check for Node #15, Program Point 47402184
KLEE: #15: Check failure due to control point not found in table
KLEE: Subsumption check for Node #16, Program Point 47402632
KLEE: #16: Check failure due to control point not found in table
KLEE: Subsumption check for Node #17, Program Point 47403976
KLEE: #17=>#5: Global check success
KLEE: Before simplification:

KLEE: Existentials not empty
KLEE: Querying for subsumption check:

KLEE: #17=>#5: Check success as solver decided validity
KLEE: Subsumption check for Node #18, Program Point 47403416
KLEE: #18=>#12: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #18=>#12: Check success as solver decided validity
KLEE: Storing entry for Node #16, Program Point 47402632
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47402632
C-File Name:Function Name:Line number = arraysimple5.c:main:49
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
KLEE: Subsumption check for Node #19, Program Point 47402296
KLEE: #19: Check failure due to control point not found in table
KLEE: Subsumption check for Node #20, Program Point 47403976
KLEE: #20=>#5: Global check success
KLEE: Before simplification:

KLEE: Existentials not empty
KLEE: Querying for subsumption check:

KLEE: #20=>#5: Check success as solver decided validity
KLEE: Subsumption check for Node #21, Program Point 47403416
KLEE: #21=>#12: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #21=>#12: Check success as solver decided validity
KLEE: Storing entry for Node #19, Program Point 47402296
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47402296
C-File Name:Function Name:Line number = arraysimple5.c:main:48
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
KLEE: Storing entry for Node #15, Program Point 47402184
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47402184
C-File Name:Function Name:Line number = arraysimple5.c:main:47
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
        ------------------------------------------
        address:
                function/value name: main/  %j = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__j)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i, __shadow__j]
KLEE: Storing entry for Node #3, Program Point 47401960
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47401960
C-File Name:Function Name:Line number = :main:0
global = []
pi = (And (Ult (ReadLSB w32 0 __shadow__i)
           4)
      (Eq false
          (Ult 2
               (ReadLSB w32 0 __shadow__j))))
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
        ------------------------------------------
        address:
                function/value name: main/  %j = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__j)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i, __shadow__j]
KLEE: Subsumption check for Node #22, Program Point 47401624
KLEE: #22: Check failure due to control point not found in table
KLEE: Subsumption check for Node #23, Program Point 47402744
KLEE: #23=>#4: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #23=>#4: Check failure as solved did not decide validity
KLEE: Subsumption check for Node #24, Program Point 47403976
KLEE: #24=>#5: Global check success
KLEE: Before simplification:

KLEE: Existentials not empty
KLEE: Querying for subsumption check:

KLEE: #24=>#5: Check success as solver decided validity
KLEE: Subsumption check for Node #25, Program Point 47403416
KLEE: #25=>#12: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #25=>#12: Check success as solver decided validity
KLEE: Storing entry for Node #23, Program Point 47402744
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47402744
C-File Name:Function Name:Line number = arraysimple5.c:main:50
global = []
pi = (And (Ult (ReadLSB w32 0 __shadow__i)
           4)
      (Ult 2
           (ReadLSB w32 0 __shadow__j)))
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
        ------------------------------------------
        address:
                function/value name: main/  %j = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__j)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i, __shadow__j]
KLEE: Subsumption check for Node #26, Program Point 47402184
KLEE: #26=>#15: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #26=>#15: Check success as solver decided validity
KLEE: Storing entry for Node #22, Program Point 47401624
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47401624
C-File Name:Function Name:Line number = arraysimple5.c:main:43
global = []
pi = (And (Ult (ReadLSB w32 0 __shadow__i)
           4)
      (Ult 2
           (ReadLSB w32 0 __shadow__j)))
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
        ------------------------------------------
        address:
                function/value name: main/  %j = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__j)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i, __shadow__j]
KLEE: Storing entry for Node #2, Program Point 47401512
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47401512
C-File Name:Function Name:Line number = arraysimple5.c:main:42
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
        ------------------------------------------
        address:
                function/value name: main/  %j = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__j)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i, __shadow__j]
KLEE: Subsumption check for Node #27, Program Point 47401176
KLEE: #27: Check failure due to control point not found in table
KLEE: Subsumption check for Node #28, Program Point 47402744
KLEE: #28=>#23: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #28=>#23: Check failure as solved did not decide validity
KLEE: #28=>#4: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #28=>#4: Check failure as solved did not decide validity
KLEE: Subsumption check for Node #29, Program Point 47403192
KLEE: #29: Check failure due to control point not found in table
KLEE: Subsumption check for Node #30, Program Point 47403976
KLEE: #30=>#5: Global check success
KLEE: Before simplification:

KLEE: Existentials not empty
KLEE: Querying for subsumption check:

KLEE: #30=>#5: Check success as solver decided validity
KLEE: Subsumption check for Node #31, Program Point 47403416
KLEE: #31=>#12: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #31=>#12: Check success as solver decided validity
KLEE: Storing entry for Node #29, Program Point 47403192
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47403192
C-File Name:Function Name:Line number = :main:0
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
KLEE: Subsumption check for Node #32, Program Point 47402856
KLEE: #32: Check failure due to control point not found in table
KLEE: Subsumption check for Node #33, Program Point 47403976
KLEE: #33=>#5: Global check success
KLEE: Before simplification:

KLEE: Existentials not empty
KLEE: Querying for subsumption check:

KLEE: #33=>#5: Check success as solver decided validity
KLEE: Subsumption check for Node #34, Program Point 47403416
KLEE: #34=>#12: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #34=>#12: Check success as solver decided validity
KLEE: Storing entry for Node #32, Program Point 47402856
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47402856
C-File Name:Function Name:Line number = arraysimple5.c:main:51
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
KLEE: Storing entry for Node #28, Program Point 47402744
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47402744
C-File Name:Function Name:Line number = arraysimple5.c:main:50
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
KLEE: Subsumption check for Node #35, Program Point 47402184
KLEE: #35=>#15: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #35=>#15: Check success as solver decided validity
KLEE: Storing entry for Node #27, Program Point 47401176
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47401176
C-File Name:Function Name:Line number = arraysimple5.c:main:40
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
        ------------------------------------------
        address:
                function/value name: main/  %j = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__j)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i, __shadow__j]
KLEE: Storing entry for Node #1, Program Point 47398936
KLEE: ------------ Subsumption Table Entry ------------
Program point = 47398936
C-File Name:Function Name:Line number = :main:0
global = []
pi = (empty)
concretely-addressed store = []
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = []
************Basic Block Coverage Report Starts****************
KLEE: done: Total number of single time Visited Basic Blocks: 24
KLEE: done: Total number of Basic Blocks: 26
************Basic Block Coverage Report Ends****************
************ICMP/Atomic Condition Coverage Report Starts****************
KLEE: done: Total number of Covered ICMP/Atomic Condition: 12
KLEE: done: Total number of All ICMP/Atomic Condition: 12
************ICMP/Atomic Condition Coverage Report Ends****************
KLEE: Memory cap NOT exceeded!

KLEE: done: Total reduced symbolic execution tree nodes = 35
KLEE: done: Total number of visited basic blocks = 72

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) = 0.026
KLEE: done:     Symbolic store expression build time (ms) = 0.001
KLEE: done:     Solver access time (ms) = 0.935
KLEE: done:     Average table entries per subsumption checkpoint = 1.10
KLEE: done:     Number of subsumption checks = 35
KLEE: done:     Average solver calls per subsumption check = 0.00

KLEE: done: TxTree method execution times (ms):
KLEE: done:     setCurrentINode = 0.33
KLEE: done:     remove = 2.045
KLEE: done:     subsumptionCheck = 1.357
KLEE: done:     markPathCondition = 0.095
KLEE: done:     split = 0.076
KLEE: done:     executeOnNode = 0.16
KLEE: done:     executeMemoryOperation = 1.163

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 0.089
KLEE: done:     addConstraintTime = 0.221
KLEE: done:     splitTime = 0.055
KLEE: done:     execute = 0.147
KLEE: done:     bindCallArguments = 0.009
KLEE: done:     bindReturnValue = 0
KLEE: done:     getStoredExpressions = 0.022
KLEE: done:     getStoredCoreExpressions = 0.078

KLEE: done: total instructions = 225
KLEE: done: completed paths = 18, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 5.5
KLEE: done:     average branching depth of subsumed paths = 4.35714
KLEE: done:     average instructions of completed paths = 118.25
KLEE: done:     average instructions of subsumed paths = 111.786
KLEE: done:     subsumed paths = 14
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(%)|
----------------------------------------------------------------------------------------
|arraysimple5-2/klee-out-0|     225|     0.03|    34.15|    27.91|     366|       63.31|

[ArpitaDutta]

WP log:

KLEE: KLEE: WATCHDOG: watching 8369

KLEE: output directory is "/home/arpita/Documents/TracerX-Work/crashes/klee-out-0"
Using Z3 solver backend
KLEE: Subsumption check for Node #1, Program Point 53133336
KLEE: #1: Check failure due to control point not found in table
KLEE: Subsumption check for Node #2, Program Point 53135912
KLEE: #2: Check failure due to control point not found in table
KLEE: Subsumption check for Node #3, Program Point 53136360
KLEE: #3: Check failure due to control point not found in table
KLEE: Subsumption check for Node #4, Program Point 53137144
KLEE: #4: Check failure due to control point not found in table
KLEE: Subsumption check for Node #5, Program Point 53138376
KLEE: #5: Check failure due to control point not found in table
KLEE: Subsumption check for Node #6, Program Point 53138824
KLEE: #6: Check failure due to control point not found in table
KLEE: Subsumption check for Node #7, Program Point 53139832
KLEE: #7: Check failure due to control point not found in table
KLEE: Storing entry for Node #7, Program Point 53139832
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53139832
C-File Name:Function Name:Line number = arraysimple5.c:main:70
global = []
pi = (empty)
concretely-addressed store = []
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = []
wp interpolant = [true]

KLEE: Subsumption check for Node #8, Program Point 53139048
KLEE: #8: Check failure due to control point not found in table
KLEE: Storing entry for Node #8, Program Point 53139048
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53139048
C-File Name:Function Name:Line number = arraysimple5.c:main:66
global = []
pi = (And (Ult N0:(ReadLSB w32 0 __shadow__i)
           4)
      (Ult N0 2))
concretely-addressed store = []
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
wp interpolant = [(Eq 97
     (Sel w32 (WPVar w32 (a))
              (ZExt w64 (WPVar w32 (i)))))]

KLEE: Storing entry for Node #6, Program Point 53138824
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53138824
C-File Name:Function Name:Line number = :main:0
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = []
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
wp interpolant = []

KLEE: Subsumption check for Node #9, Program Point 53138488
KLEE: #9: Check failure due to control point not found in table
KLEE: Subsumption check for Node #10, Program Point 53139832
KLEE: #10=>#7: Global check success
KLEE: #10=>#7: Weakest precondition check success
KLEE: #10=>#7: Check success due to empty table entry
KLEE: Subsumption check for Node #11, Program Point 53139048
KLEE: #11=>#8: Global check success
KLEE: WARNING: instantiateWPatSubsumption: unable to instantiate for non-constant array index!
KLEE: Storing entry for Node #11, Program Point 53139048
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53139048
C-File Name:Function Name:Line number = arraysimple5.c:main:66
global = []
pi = (And (Ult N0:(ReadLSB w32 0 __shadow__i)
           4)
      (Ult N0 2))
concretely-addressed store = []
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
wp interpolant = [(Eq 97
     (Sel w32 (WPVar w32 (a))
              (ZExt w64 (WPVar w32 (i)))))]

KLEE: Storing entry for Node #9, Program Point 53138488
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53138488
C-File Name:Function Name:Line number = arraysimple5.c:main:59
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = []
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
wp interpolant = []

KLEE: Storing entry for Node #5, Program Point 53138376
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53138376
C-File Name:Function Name:Line number = arraysimple5.c:main:58
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = []
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
wp interpolant = []

KLEE: Subsumption check for Node #12, Program Point 53137816
KLEE: #12: Check failure due to control point not found in table
KLEE: Subsumption check for Node #13, Program Point 53138264
KLEE: #13: Check failure due to control point not found in table
KLEE: Storing entry for Node #13, Program Point 53138264
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53138264
C-File Name:Function Name:Line number = arraysimple5.c:main:57
global = []
pi = (And (Ult N0:(ReadLSB w32 0 __shadow__i)
           4)
      (Eq false (Ult 1 N0)))
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
wp interpolant = []

KLEE: Subsumption check for Node #14, Program Point 53137928
KLEE: #14: Check failure due to control point not found in table
KLEE: Storing entry for Node #14, Program Point 53137928
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53137928
C-File Name:Function Name:Line number = arraysimple5.c:main:56
global = []
pi = (Ult 1
      (ReadLSB w32 0 __shadow__i))
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
wp interpolant = []

KLEE: Storing entry for Node #12, Program Point 53137816
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53137816
C-File Name:Function Name:Line number = arraysimple5.c:main:55
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
wp interpolant = []

KLEE: Storing entry for Node #4, Program Point 53137144
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53137144
C-File Name:Function Name:Line number = arraysimple5.c:main:50
global = []
pi = (And (Ult (ReadLSB w32 0 __shadow__i)
           4)
      (Eq false
          (Ult 2
               (ReadLSB w32 0 __shadow__j))))
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
        ------------------------------------------
        address:
                function/value name: main/  %j = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__j)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i, __shadow__j]
wp interpolant = []

KLEE: Subsumption check for Node #15, Program Point 53136584
KLEE: #15: Check failure due to control point not found in table
KLEE: Subsumption check for Node #16, Program Point 53137032
KLEE: #16: Check failure due to control point not found in table
KLEE: Subsumption check for Node #17, Program Point 53138376
KLEE: #17=>#5: Global check success
KLEE: Before simplification:

KLEE: Existentials not empty
KLEE: Querying for subsumption check:

KLEE: #17=>#5: Check success as solver decided validity
KLEE: Subsumption check for Node #18, Program Point 53137816
KLEE: #18=>#12: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #18=>#12: Check success as solver decided validity
KLEE: Storing entry for Node #16, Program Point 53137032
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53137032
C-File Name:Function Name:Line number = arraysimple5.c:main:49
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
wp interpolant = []

KLEE: Subsumption check for Node #19, Program Point 53136696
KLEE: #19: Check failure due to control point not found in table
KLEE: Subsumption check for Node #20, Program Point 53138376
KLEE: #20=>#5: Global check success
KLEE: Before simplification:

KLEE: Existentials not empty
KLEE: Querying for subsumption check:

KLEE: #20=>#5: Check success as solver decided validity
KLEE: Subsumption check for Node #21, Program Point 53137816
KLEE: #21=>#12: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #21=>#12: Check success as solver decided validity
KLEE: Storing entry for Node #19, Program Point 53136696
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53136696
C-File Name:Function Name:Line number = arraysimple5.c:main:48
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
wp interpolant = []

KLEE: Storing entry for Node #15, Program Point 53136584
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53136584
C-File Name:Function Name:Line number = arraysimple5.c:main:47
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
        ------------------------------------------
        address:
                function/value name: main/  %j = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__j)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i, __shadow__j]
wp interpolant = []

KLEE: Storing entry for Node #3, Program Point 53136360
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53136360
C-File Name:Function Name:Line number = :main:0
global = []
pi = (And (Ult (ReadLSB w32 0 __shadow__i)
           4)
      (Eq false
          (Ult 2
               (ReadLSB w32 0 __shadow__j))))
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
        ------------------------------------------
        address:
                function/value name: main/  %j = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__j)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i, __shadow__j]
wp interpolant = []

KLEE: Subsumption check for Node #22, Program Point 53136024
KLEE: #22: Check failure due to control point not found in table
KLEE: Subsumption check for Node #23, Program Point 53137144
KLEE: #23=>#4: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #23=>#4: Check failure as solved did not decide validity
KLEE: Subsumption check for Node #24, Program Point 53138376
KLEE: #24=>#5: Global check success
KLEE: Before simplification:

KLEE: Existentials not empty
KLEE: Querying for subsumption check:

KLEE: #24=>#5: Check success as solver decided validity
KLEE: Subsumption check for Node #25, Program Point 53137816
KLEE: #25=>#12: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #25=>#12: Check success as solver decided validity
KLEE: Storing entry for Node #23, Program Point 53137144
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53137144
C-File Name:Function Name:Line number = arraysimple5.c:main:50
global = []
pi = (And (Ult (ReadLSB w32 0 __shadow__i)
           4)
      (Ult 2
           (ReadLSB w32 0 __shadow__j)))
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
        ------------------------------------------
        address:
                function/value name: main/  %j = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__j)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i, __shadow__j]
wp interpolant = []

KLEE: Subsumption check for Node #26, Program Point 53136584
KLEE: #26=>#15: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #26=>#15: Check success as solver decided validity
KLEE: Storing entry for Node #22, Program Point 53136024
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53136024
C-File Name:Function Name:Line number = arraysimple5.c:main:43
global = []
pi = (And (Ult (ReadLSB w32 0 __shadow__i)
           4)
      (Ult 2
           (ReadLSB w32 0 __shadow__j)))
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
        ------------------------------------------
        address:
                function/value name: main/  %j = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__j)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i, __shadow__j]
wp interpolant = []

KLEE: Storing entry for Node #2, Program Point 53135912
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53135912
C-File Name:Function Name:Line number = arraysimple5.c:main:42
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
        ------------------------------------------
        address:
                function/value name: main/  %j = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__j)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i, __shadow__j]
wp interpolant = []

KLEE: Subsumption check for Node #27, Program Point 53135576
KLEE: #27: Check failure due to control point not found in table
KLEE: Subsumption check for Node #28, Program Point 53137144
KLEE: #28=>#23: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #28=>#23: Check failure as solved did not decide validity
KLEE: #28=>#4: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #28=>#4: Check failure as solved did not decide validity
KLEE: Subsumption check for Node #29, Program Point 53137592
KLEE: #29: Check failure due to control point not found in table
KLEE: Subsumption check for Node #30, Program Point 53138376
KLEE: #30=>#5: Global check success
KLEE: Before simplification:

KLEE: Existentials not empty
KLEE: Querying for subsumption check:

KLEE: #30=>#5: Check success as solver decided validity
KLEE: Subsumption check for Node #31, Program Point 53137816
KLEE: #31=>#12: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #31=>#12: Check success as solver decided validity
KLEE: Storing entry for Node #29, Program Point 53137592
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53137592
C-File Name:Function Name:Line number = :main:0
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
wp interpolant = []

KLEE: Subsumption check for Node #32, Program Point 53137256
KLEE: #32: Check failure due to control point not found in table
KLEE: Subsumption check for Node #33, Program Point 53138376
KLEE: #33=>#5: Global check success
KLEE: Before simplification:

KLEE: Existentials not empty
KLEE: Querying for subsumption check:

KLEE: #33=>#5: Check success as solver decided validity
KLEE: Subsumption check for Node #34, Program Point 53137816
KLEE: #34=>#12: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #34=>#12: Check success as solver decided validity
KLEE: Storing entry for Node #32, Program Point 53137256
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53137256
C-File Name:Function Name:Line number = arraysimple5.c:main:51
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
wp interpolant = []

KLEE: Storing entry for Node #28, Program Point 53137144
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53137144
C-File Name:Function Name:Line number = arraysimple5.c:main:50
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i]
wp interpolant = []

KLEE: Subsumption check for Node #35, Program Point 53136584
KLEE: #35=>#15: Global check success
KLEE: Before simplification:

KLEE: Querying for subsumption check:

KLEE: #35=>#15: Check success as solver decided validity
KLEE: Storing entry for Node #27, Program Point 53135576
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53135576
C-File Name:Function Name:Line number = arraysimple5.c:main:40
global = []
pi = (Ult (ReadLSB w32 0 __shadow__i)
      4)
concretely-addressed store = [
        address:
                function/value name: main/  %i = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__i)
        ------------------------------------------
        address:
                function/value name: main/  %j = alloca i32, align 4
        content:
                (ReadLSB w32 0 __shadow__j)
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = [__shadow__i, __shadow__j]
wp interpolant = []

KLEE: Storing entry for Node #1, Program Point 53133336
KLEE: ------------ Subsumption Table Entry ------------
Program point = 53133336
C-File Name:Function Name:Line number = :main:0
global = []
pi = (empty)
concretely-addressed store = []
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = []
wp interpolant = []

************Basic Block Coverage Report Starts****************
KLEE: done: Total number of single time Visited Basic Blocks: 24
KLEE: done: Total number of Basic Blocks: 26
************Basic Block Coverage Report Ends****************
************ICMP/Atomic Condition Coverage Report Starts****************
KLEE: done: Total number of Covered ICMP/Atomic Condition: 12
KLEE: done: Total number of All ICMP/Atomic Condition: 12
************ICMP/Atomic Condition Coverage Report Ends****************
KLEE: Memory cap NOT exceeded!

KLEE: done: Total reduced symbolic execution tree nodes = 35
KLEE: done: Total number of visited basic blocks = 75

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) = 0.032
KLEE: done:     Symbolic store expression build time (ms) = 0
KLEE: done:     Solver access time (ms) = 1.173
KLEE: done:     Average table entries per subsumption checkpoint = 1.15
KLEE: done:     Number of subsumption checks = 35
KLEE: done:     Average solver calls per subsumption check = 0.00

KLEE: done: TxTree method execution times (ms):
KLEE: done:     setCurrentINode = 0.544
KLEE: done:     remove = 3.283
KLEE: done:     subsumptionCheck = 1.785
KLEE: done:     markPathCondition = 0.257
KLEE: done:     split = 0.104
KLEE: done:     executeOnNode = 0.38
KLEE: done:     executeMemoryOperation = 1.66

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 0.181
KLEE: done:     get WP Interpolant = 0.068
KLEE: done:     addConstraintTime = 0.294
KLEE: done:     splitTime = 0.08
KLEE: done:     execute = 0.347
KLEE: done:     bindCallArguments = 0.046
KLEE: done:     bindReturnValue = 0.003
KLEE: done:     getStoredExpressions = 0.027
KLEE: done:     getStoredCoreExpressions = 0.124

KLEE: done: total instructions = 235
KLEE: done: completed paths = 18, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 5.6
KLEE: done:     average branching depth of subsumed paths = 4.23077
KLEE: done:     average instructions of completed paths = 120
KLEE: done:     average instructions of subsumed paths = 111.308
KLEE: done:     subsumed paths = 13
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 5
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.
'arraysimple5-3' already present. Replacing with a new folder
cp: cannot stat 'allfigs2pdf3': No such file or directory
----------------------------------------------------------------------------------------
|          Path           |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
----------------------------------------------------------------------------------------
|arraysimple5-3/klee-out-0|     235|     0.05|    34.15|    27.91|     366|       64.75|
----------------------------------------------------------------------------------------

[rasoolmaghareh]

Thanks @ArpitaDutta Closing this issue.