Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

TestCompBug: Unmatched output for 'rule57_ebda_blast_2' #407

Open
ArpitaDutta opened this issue Jan 6, 2024 · 0 comments
Open

TestCompBug: Unmatched output for 'rule57_ebda_blast_2' #407

ArpitaDutta opened this issue Jan 6, 2024 · 0 comments

Comments

@ArpitaDutta
Copy link
Member

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 c52030b":
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|
-----------------------------------------------------------------------------------------------
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant