clang -emit-llvm -g -I/usr/local/lib/tracerx/include -I/usr/local/lib/tracerx/../include -Wno-int-conversion -c joxan-wp-sim.c joxan-wp-sim.c:9:9: warning: implicit declaration of function 'choice' is invalid in C99 [-Wimplicit-function-declaration] c = choice(a); ^ joxan-wp-sim.c:10:18: warning: implicitly declaring library function 'exit' with type 'void (int) __attribute__((noreturn))' if (c == -1) exit(0); ^ joxan-wp-sim.c:10:18: note: please include the header or explicitly provide a declaration for 'exit' joxan-wp-sim.c:12:5: warning: implicit declaration of function '__assert_fail' is invalid in C99 [-Wimplicit-function-declaration] klee_assert(sum <= 9000); ^ /usr/local/lib/tracerx/include/klee/klee.h:96:6: note: expanded from macro 'klee_assert' : __assert_fail (#expr, __FILE__, __LINE__, __PRETTY_FUNCTION__)) \ ^ 3 warnings generated. SOLVER_FLAGS="-solver-backend=z3" OUTPUT_DIR=joxan-wp-sim.tx make joxan-wp-sim.klee-out make[1]: Entering directory '/home/sajjad/Tracer-X/klee-examples/basic' KLEE: output directory is "/home/sajjad/Tracer-X/klee-examples/basic/joxan-wp-sim.tx" Using Z3 solver backend KLEE: Logging all queries in .pc format to /home/sajjad/Tracer-X/klee-examples/basic/joxan-wp-sim.tx/all-queries.pc KLEE: Logging all queries in .smt2 format to /home/sajjad/Tracer-X/klee-examples/basic/joxan-wp-sim.tx/all-queries.smt2 KLEE: Deterministic memory allocation starting from 0x7ff30000000 KLEE: Subsumption check for Node #1, Program Point 36285272 KLEE: #1: Check failure due to control point not found in table KLEE: Subsumption check for Node #2, Program Point 36330680 KLEE: #2: Check failure due to control point not found in table KLEE: Storing entry for Node #2, Program Point 36330680 KLEE: ------------ Subsumption Table Entry ------------ Program point = 36330680 interpolant = (empty) concretely-addressed store = [ address: function/value: @a = global [5 x i32] [i32 1, i32 10, i32 100, i32 1000, i32 -1], align 16 stack: (empty) offset: 0 content: function/value: choice/ %2 = load i32* %1, align 4, !dbg !140 1 reason(s) for storage: branch infeasibility [main: Line 10] ] symbolically-addressed store = [] concretely-addressed historical store = [] symbolically-addressed historical store = [] existentials = [] wp interpolant = [(And (Sle (Add w32 (WPVar w32 (sum)) N0:(Sel w32 (WPVar w32 (a.addr)) 0)) 9000) (Not (Eq 4294967295 N0)))] KLEE: Subsumption check for Node #3, Program Point 36329976 KLEE: #3: Check failure due to control point not found in table KLEE: Subsumption check for Node #4, Program Point 36330680 KLEE: #4: Check failure due to entry not found KLEE: Storing entry for Node #4, Program Point 36330680 KLEE: ------------ Subsumption Table Entry ------------ Program point = 36330680 interpolant = (empty) concretely-addressed store = [ address: function/value: @a = global [5 x i32] [i32 1, i32 10, i32 100, i32 1000, i32 -1], align 16 stack: (empty) offset: 4 content: function/value: choice/ %2 = load i32* %1, align 4, !dbg !140 10 reason(s) for storage: branch infeasibility [main: Line 10] ] symbolically-addressed store = [] concretely-addressed historical store = [] symbolically-addressed historical store = [] existentials = [] wp interpolant = [(And (Sle (Add w32 (WPVar w32 (sum)) N0:(Sel w32 (WPVar w32 (a.addr)) 0)) 9000) (Not (Eq 4294967295 N0)))] KLEE: Subsumption check for Node #5, Program Point 36329976 KLEE: #5: Check failure due to control point not found in table KLEE: Subsumption check for Node #6, Program Point 36330680 KLEE: #6: Check failure due to entry not found KLEE: Storing entry for Node #6, Program Point 36330680 KLEE: ------------ Subsumption Table Entry ------------ Program point = 36330680 interpolant = (empty) concretely-addressed store = [ address: function/value: @a = global [5 x i32] [i32 1, i32 10, i32 100, i32 1000, i32 -1], align 16 stack: (empty) offset: 8 content: function/value: choice/ %2 = load i32* %1, align 4, !dbg !140 100 reason(s) for storage: branch infeasibility [main: Line 10] ] symbolically-addressed store = [] concretely-addressed historical store = [] symbolically-addressed historical store = [] existentials = [] wp interpolant = [(And (Sle (Add w32 (WPVar w32 (sum)) N0:(Sel w32 (WPVar w32 (a.addr)) 0)) 9000) (Not (Eq 4294967295 N0)))] KLEE: Subsumption check for Node #7, Program Point 36329976 KLEE: #7: Check failure due to control point not found in table KLEE: Subsumption check for Node #8, Program Point 36330680 KLEE: #8: Check failure due to entry not found KLEE: Storing entry for Node #8, Program Point 36330680 KLEE: ------------ Subsumption Table Entry ------------ Program point = 36330680 interpolant = (empty) concretely-addressed store = [ address: function/value: @a = global [5 x i32] [i32 1, i32 10, i32 100, i32 1000, i32 -1], align 16 stack: (empty) offset: 12 content: function/value: choice/ %2 = load i32* %1, align 4, !dbg !140 1000 reason(s) for storage: branch infeasibility [main: Line 10] ] symbolically-addressed store = [] concretely-addressed historical store = [] symbolically-addressed historical store = [] existentials = [] wp interpolant = [(And (Sle (Add w32 (WPVar w32 (sum)) N0:(Sel w32 (WPVar w32 (a.addr)) 0)) 9000) (Not (Eq 4294967295 N0)))] KLEE: Subsumption check for Node #9, Program Point 36329976 KLEE: #9: Check failure due to control point not found in table KLEE: Storing entry for Node #9, Program Point 36329976 %1 = load i32** %a.addr, align 8, !dbg !140 KLEE: WARNING: TxWeakestPreCondition::getLoad: Not implemented yet! KLEE: ------------ Subsumption Table Entry ------------ Program point = 36329976 interpolant = (empty) concretely-addressed store = [ address: function/value: @a = global [5 x i32] [i32 1, i32 10, i32 100, i32 1000, i32 -1], align 16 stack: (empty) offset: 12 content: function/value: choice/ %2 = load i32* %1, align 4, !dbg !140 1000 reason(s) for storage: branch infeasibility [choice: Line 18] ------------------------------------------ address: function/value: choice/ %a.addr = alloca i32*, align 8 stack: %call = call i32 @choice(i32* %add.ptr), !dbg !142 %call = call i32 @choice(i32* %add.ptr), !dbg !142 %call = call i32 @choice(i32* %add.ptr), !dbg !142 %call = call i32 @choice(i32* getelementptr inbounds ([5 x i32]* @a, i32 0, i32 0)), !dbg !139 offset: 0 content: function/value: i32* %a OFFSETS: [[base: 8792603361336, size: 20]=={12}] reason(s) for storage: branch infeasibility [choice: Line 18] pointer use [choice: Line 18] ] symbolically-addressed store = [] concretely-addressed historical store = [] symbolically-addressed historical store = [] existentials = [] wp interpolant = [] KLEE: Storing entry for Node #7, Program Point 36329976 KLEE: ------------ Subsumption Table Entry ------------ Program point = 36329976 interpolant = (empty) concretely-addressed store = [ address: function/value: @a = global [5 x i32] [i32 1, i32 10, i32 100, i32 1000, i32 -1], align 16 stack: (empty) offset: 8 content: function/value: choice/ %2 = load i32* %1, align 4, !dbg !140 100 reason(s) for storage: branch infeasibility [choice: Line 18] ------------------------------------------ address: function/value: choice/ %a.addr = alloca i32*, align 8 stack: %call = call i32 @choice(i32* %add.ptr), !dbg !142 %call = call i32 @choice(i32* %add.ptr), !dbg !142 %call = call i32 @choice(i32* getelementptr inbounds ([5 x i32]* @a, i32 0, i32 0)), !dbg !139 offset: 0 content: function/value: i32* %a OFFSETS: [[base: 8792603361336, size: 20]=={8}] reason(s) for storage: branch infeasibility [choice: Line 18] pointer use [choice: Line 18] ] symbolically-addressed store = [] concretely-addressed historical store = [] symbolically-addressed historical store = [] existentials = [] wp interpolant = [] KLEE: Storing entry for Node #5, Program Point 36329976 KLEE: ------------ Subsumption Table Entry ------------ Program point = 36329976 interpolant = (empty) concretely-addressed store = [ address: function/value: @a = global [5 x i32] [i32 1, i32 10, i32 100, i32 1000, i32 -1], align 16 stack: (empty) offset: 4 content: function/value: choice/ %2 = load i32* %1, align 4, !dbg !140 10 reason(s) for storage: branch infeasibility [choice: Line 18] ------------------------------------------ address: function/value: choice/ %a.addr = alloca i32*, align 8 stack: %call = call i32 @choice(i32* %add.ptr), !dbg !142 %call = call i32 @choice(i32* getelementptr inbounds ([5 x i32]* @a, i32 0, i32 0)), !dbg !139 offset: 0 content: function/value: i32* %a OFFSETS: [[base: 8792603361336, size: 20]=={4}] reason(s) for storage: branch infeasibility [choice: Line 18] pointer use [choice: Line 18] ] symbolically-addressed store = [] concretely-addressed historical store = [] symbolically-addressed historical store = [] existentials = [] wp interpolant = [] KLEE: Storing entry for Node #3, Program Point 36329976 KLEE: ------------ Subsumption Table Entry ------------ Program point = 36329976 interpolant = (empty) concretely-addressed store = [ address: function/value: @a = global [5 x i32] [i32 1, i32 10, i32 100, i32 1000, i32 -1], align 16 stack: (empty) offset: 0 content: function/value: choice/ %2 = load i32* %1, align 4, !dbg !140 1 reason(s) for storage: branch infeasibility [choice: Line 18] ------------------------------------------ address: function/value: choice/ %a.addr = alloca i32*, align 8 stack: %call = call i32 @choice(i32* getelementptr inbounds ([5 x i32]* @a, i32 0, i32 0)), !dbg !139 offset: 0 content: function/value: i32* %a OFFSETS: [[base: 8792603361336, size: 20]=={0}] reason(s) for storage: branch infeasibility [choice: Line 18] pointer use [choice: Line 18] ] symbolically-addressed store = [] concretely-addressed historical store = [] symbolically-addressed historical store = [] existentials = [] wp interpolant = [] KLEE: Storing entry for Node #1, Program Point 36285272 KLEE: ------------ Subsumption Table Entry ------------ Program point = 36285272 interpolant = (empty) concretely-addressed store = [] symbolically-addressed store = [] concretely-addressed historical store = [] symbolically-addressed historical store = [] existentials = [] wp interpolant = [] KLEE: Deterministic memory allocation starting from 0x7ff30000000 KLEE: Memory cap NOT exceeded! KLEE: done: Total reduced symbolic execution tree nodes = 9 KLEE: done: Total number of visited basic blocks = 42 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 KLEE: done: Symbolic store expression build time (ms) = 0 KLEE: done: Solver access time (ms) = 0 KLEE: done: Average table entries per subsumption checkpoint = 3.00 KLEE: done: Number of subsumption checks = 9 KLEE: done: Average solver calls per subsumption check = 0.00 KLEE: done: TxTree method execution times (ms): KLEE: done: setCurrentINode = 0.149 KLEE: done: remove = 41.547 KLEE: done: subsumptionCheck = 0.129 KLEE: done: markPathCondition = 0.053 KLEE: done: split = 0.028 KLEE: done: executeOnNode = 0.122 KLEE: done: executeMemoryOperation = 0.875 KLEE: done: TxTreeNode method execution times (ms): KLEE: done: getInterpolant = 0.005 KLEE: done: get WP Interpolant = 38.899 KLEE: done: addConstraintTime = 0.075 KLEE: done: splitTime = 0.021 KLEE: done: execute = 0.116 KLEE: done: bindCallArguments = 0.02 KLEE: done: bindReturnValue = 0.015 KLEE: done: getStoredExpressions = 0 KLEE: done: getStoredCoreExpressions = 0.062 KLEE: done: total instructions = 211 KLEE: done: completed paths = 5, among which KLEE: done: early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0 KLEE: done: average branching depth of completed paths = 2.8 KLEE: done: average branching depth of subsumed paths = 0 KLEE: done: average instructions of completed paths = 73.2 KLEE: done: average instructions of subsumed paths = 0 KLEE: done: subsumed paths = 0 KLEE: done: error paths = 0 KLEE: done: program exit paths = 5 KLEE: done: generated tests = 3, 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 = 3 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. 0.05user 0.00system 0:00.06elapsed 98%CPU (0avgtext+0avgdata 33496maxresident)k 0inputs+296outputs (0major+1617minor)pagefaults 0swaps make[2]: Entering directory '/home/sajjad/Tracer-X/klee-examples/basic' Writing 'cfg.main.dot'... Writing 'cfg.choice.dot'... Printing analysis 'Print CFG of function to 'dot' file' for function 'main': Printing analysis 'Print CFG of function to 'dot' file' for function 'choice': ------------------------------------------------------------------------------ | Path | Instrs| Time(s)| ICov(%)| BCov(%)| ICount| TSolver(%)| ------------------------------------------------------------------------------ |joxan-wp-sim.tx| 211| 0.05| 14.84| 9.46| 310| 8.88| ------------------------------------------------------------------------------ make[2]: Leaving directory '/home/sajjad/Tracer-X/klee-examples/basic' make[1]: Leaving directory '/home/sajjad/Tracer-X/klee-examples/basic' rm joxan-wp-sim.bc