Skip to content
Snippets Groups Projects
Commit ed91c31c authored by David Bühler's avatar David Bühler
Browse files

[Eva] Removes unused oracle.

parent bfd7425d
No related branches found
No related tags found
No related merge requests found
[kernel] Parsing tests/misc/unroll_annots.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
a[0..9] ∈ {0}
b[0..9] ∈ {0}
[eva:loop-unroll] tests/misc/unroll_annots.c:8: loop not completely unrolled
[eva] tests/misc/unroll_annots.c:8: starting to merge loop iterations
[eva:loop-unroll] tests/misc/unroll_annots.c:14: loop not completely unrolled
[eva] tests/misc/unroll_annots.c:14: starting to merge loop iterations
[eva] tests/misc/unroll_annots.c:16: starting to merge loop iterations
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
a[0..9] ∈ {42}
b[0..9] ∈ {42}
__retres ∈ {0}
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function main:
a[0..9] FROM \nothing (and SELF)
b[0..9] FROM \nothing (and SELF)
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
a[0..9]; b[0..9]; i; j; i_0; j_0; __retres
[inout] Inputs for function main:
\nothing
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment