tracer-x / TracerX

TracerX Symbolic Virtual Machine
https://tracer-x.github.io/
Other
31 stars 11 forks source link

TestCompBug: Unmatched output for 'rule57_ebda_blast_2' #407

Open ArpitaDutta opened 9 months ago

ArpitaDutta commented 9 months ago

On TestComp-24 setup, the output generated for program "rule57_ebda_blast_2" is here))).

Whereas, on running the same program (TracerX-version) on TracerX setup "commit c52030b91c0d63f6a1483367ea9b4461bd2b9447": The output obtained is as follows:


rule57_ebda_blast_2.c:58:36: warning: unknown attribute '__leaf__' ignored [-Wattributes]
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
                                   ^
1 warning generated.
KLEE: KLEE: WATCHDOG: watching 5965

KLEE: output directory is "/home/arpita/Documents/TestCompAnalysis/klee-out-0"
Using Z3 solver backend
KLEE: WARNING: using default handler for external function calloc
KLEE: WARNING: using default handler for external function calloc
KLEE: WARNING: using default handler for external function calloc
  %6 = bitcast %struct.slot* %5 to i8*, !dbg !168
KLEE: WARNING: TxWeakestPreCondition::generateExprFromOperand Unary Operand not implemented...

  %6 = bitcast %struct.slot* %5 to i8*, !dbg !168
KLEE: WARNING: TxWeakestPreCondition::generateExprFromOperand Unary Operand not implemented...

KLEE: ERROR: /home/arpita/Documents/TestCompAnalysis/rule57_ebda_blast_2.c:7: ASSERTION FAIL: 0
KLEE: NOTE: now ignoring this error at this location
************Basic Block Coverage Report Starts****************
KLEE: done: Total number of single time Visited Basic Blocks: 32
KLEE: done: Total number of Basic Blocks: 38
************Basic Block Coverage Report Ends****************
************ICMP/Atomic Condition Coverage Report Starts****************
KLEE: done: Total number of Covered ICMP/Atomic Condition: 10
KLEE: done: Total number of All ICMP/Atomic Condition: 10
************ICMP/Atomic Condition Coverage Report Ends****************
KLEE: Memory cap NOT exceeded!

KLEE: done: Total reduced symbolic execution tree nodes = 7
KLEE: done: Total number of visited basic blocks = 39

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 = 1.00
KLEE: done:     Number of subsumption checks = 7
KLEE: done:     Average solver calls per subsumption check = 0.00

KLEE: done: TxTree method execution times (ms):
KLEE: done:     setCurrentINode = 0.353
KLEE: done:     remove = 1.173
KLEE: done:     subsumptionCheck = 0.003
KLEE: done:     markPathCondition = 0.079
KLEE: done:     split = 0.061
KLEE: done:     executeOnNode = 0.6
KLEE: done:     executeMemoryOperation = 1.612

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 0.001
KLEE: done:     get WP Interpolant = 0.755
KLEE: done:     addConstraintTime = 0.159
KLEE: done:     splitTime = 0.05
KLEE: done:     execute = 0.557
KLEE: done:     bindCallArguments = 0.058
KLEE: done:     bindReturnValue = 0.038
KLEE: done:     getStoredExpressions = 0
KLEE: done:     getStoredCoreExpressions = 0.102

KLEE: done: total instructions = 233
KLEE: done: completed paths = 4, 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.25
KLEE: done:     average branching depth of subsumed paths = 0
KLEE: done:     average instructions of completed paths = 128
KLEE: done:     average instructions of subsumed paths = 0
KLEE: done:     subsumed paths = 0
KLEE: done:     error paths = 1
KLEE: done:     program exit paths = 3
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(%)|
-----------------------------------------------------------------------------------------------
|rule57_ebda_blast_2-3/klee-out-0|     233|     0.03|    34.14|    18.60|     413|       23.32|
-----------------------------------------------------------------------------------------------