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

[Eva] Adds a test for the evaluation of "calls" annotations.

parent 0560e941
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/value/calls_annotation.i 0 → 100644
+ 101
− 0
View file @ 8a310a69
/* run.config*
STDOPT:
*/
/* This file tests the evaluation of the logical status of "calls" annotations,
and the reduction of called functions accordingly. */
volatile unsigned int nondet;
int incr(int x) {
return x+1;
}
int decr(int x) {
return x-1;
}
int square(int x) {
return x*x;
}
/* Should be never called according to "calls" annotations. */
int error(int x) {
return x / 0;
}
int unreachable(int x) {
return 0;
}
typedef int (*fptr)(int);
fptr funs[4] = { &incr, &decr, &square, &error };
int apply(fptr fp, int a) {
int x;
//@ calls incr, decr, square; // unknown: error could also be called
x = (*fp)(a);
//@ calls incr, decr, square; // valid as consequence of the previous one
x = (*fp)(x);
return x;
}
void main(void) {
int a = 1, i = 0;
/* Valid "calls" annotations. */
//@ calls decr; // valid singleton
a = (*funs[1])(a);
i = nondet % 3;
//@ calls incr, decr, square; // valid
a = (*funs[i])(a);
//@ calls incr, decr, square, unreachable; // valid but contains unreachable
a = (*funs[i])(a);
/* Unknown "calls" annotations: Eva can reduce the called functions. */
i = nondet % 4;
//@ calls incr, decr; // unknown: square and error could also be called
a = (*funs[i])(a);
Frama_C_show_each_0_1(i); // i can be reduced to {0; 1}
/* Invalid "calls" annotations. */
if (nondet) {
//@ calls incr; // invalid
a = (*funs[1])(a);
Frama_C_show_each_UNREACHABLE();
}
if (nondet) {
i = nondet % 2;
//@ calls square, unreachable; // invalid
a = (*funs[i])(a);
Frama_C_show_each_UNREACHABLE(i);
}
/* "calls" annotations evaluated in multiple states. */
//@ loop unroll 4;
for (int j = 0; j < 4; j++) {
a = 0;
//@ calls incr; // valid at each iteration
a = (*funs[0])(a);
//@ calls incr, decr; // valid at each iteration
a = (*funs[j % 2])(a);
i = nondet % (j+1);
//@ calls incr, decr, square; // valid then unknown at the last iteration
a = (*funs[i])(a);
if (nondet) {
//@ calls incr, decr, square; // invalid at the last iteration
a = (*funs[j])(a);
if (j == 3) Frama_C_show_each_UNREACHABLE(j); // j == 3 is impossible here.
}
if (nondet) {
a = apply(funs[j], a); // invalid at the last iteration
if (j == 3) Frama_C_show_each_UNREACHABLE(j); // j == 3 is impossible here.
}
if (nondet) {
//@ calls unreachable; // invalid at each iteration
a = (*funs[j])(a);
Frama_C_show_each_UNREACHABLE(a);
}
}
}
tests/value/oracle/calls_annotation.res.oracle 0 → 100644
+ 209
− 0
View file @ 8a310a69
[kernel] Parsing calls_annotation.i (no 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
nondet ∈ [--..--]
funs[0] ∈ {{ &incr }}
[1] ∈ {{ &decr }}
[2] ∈ {{ &square }}
[3] ∈ {{ &error }}
[eva] calls_annotation.i:49: calls annotation got status valid.
[eva] computing for function decr <- main.
Called from calls_annotation.i:49.
[eva] Recording results for decr
[eva] Done for function decr
[eva] calls_annotation.i:52: calls annotation got status valid.
[eva] computing for function square <- main.
Called from calls_annotation.i:52.
[eva] Recording results for square
[eva] Done for function square
[eva] computing for function decr <- main.
Called from calls_annotation.i:52.
[eva] Recording results for decr
[eva] Done for function decr
[eva] computing for function incr <- main.
Called from calls_annotation.i:52.
[eva] Recording results for incr
[eva] Done for function incr
[eva] calls_annotation.i:54: calls annotation got status valid.
[eva] computing for function square <- main.
Called from calls_annotation.i:54.
[eva] Recording results for square
[eva] Done for function square
[eva] computing for function decr <- main.
Called from calls_annotation.i:54.
[eva] Recording results for decr
[eva] Done for function decr
[eva] computing for function incr <- main.
Called from calls_annotation.i:54.
[eva] Recording results for incr
[eva] Done for function incr
[eva:alarm] calls_annotation.i:59: Warning: calls annotation got status unknown.
[eva] computing for function decr <- main.
Called from calls_annotation.i:59.
[eva] Recording results for decr
[eva] Done for function decr
[eva] computing for function incr <- main.
Called from calls_annotation.i:59.
[eva] Recording results for incr
[eva] Done for function incr
[eva] calls_annotation.i:60: Frama_C_show_each_0_1: {0; 1}
[eva:alarm] calls_annotation.i:65: Warning:
calls annotation got status invalid (stopping propagation).
[eva:alarm] calls_annotation.i:71: Warning:
calls annotation got status invalid (stopping propagation).
[eva] calls_annotation.i:80: calls annotation got status valid.
[eva] calls_annotation.i:80: Reusing old results for call to incr
[eva] calls_annotation.i:82: calls annotation got status valid.
[eva] computing for function incr <- main.
Called from calls_annotation.i:82.
[eva] Recording results for incr
[eva] Done for function incr
[eva] calls_annotation.i:85: calls annotation got status valid.
[eva] computing for function incr <- main.
Called from calls_annotation.i:85.
[eva] Recording results for incr
[eva] Done for function incr
[eva] calls_annotation.i:88: calls annotation got status valid.
[eva] computing for function incr <- main.
Called from calls_annotation.i:88.
[eva] Recording results for incr
[eva] Done for function incr
[eva] computing for function apply <- main.
Called from calls_annotation.i:92.
[eva] calls_annotation.i:38: calls annotation got status valid.
[eva] computing for function incr <- apply <- main.
Called from calls_annotation.i:38.
[eva] Recording results for incr
[eva] Done for function incr
[eva] calls_annotation.i:40: calls annotation got status valid.
[eva] computing for function incr <- apply <- main.
Called from calls_annotation.i:40.
[eva] Recording results for incr
[eva] Done for function incr
[eva] Recording results for apply
[eva] Done for function apply
[eva:alarm] calls_annotation.i:97: Warning:
calls annotation got status invalid (stopping propagation).
[eva] calls_annotation.i:80: Reusing old results for call to incr
[eva] calls_annotation.i:82: Reusing old results for call to decr
[eva] calls_annotation.i:85: Reusing old results for call to decr
[eva] calls_annotation.i:85: Reusing old results for call to incr
[eva] computing for function decr <- main.
Called from calls_annotation.i:88.
[eva] Recording results for decr
[eva] Done for function decr
[eva] computing for function apply <- main.
Called from calls_annotation.i:92.
[eva] computing for function decr <- apply <- main.
Called from calls_annotation.i:38.
[eva] Recording results for decr
[eva] Done for function decr
[eva] computing for function decr <- apply <- main.
Called from calls_annotation.i:40.
[eva] Recording results for decr
[eva] Done for function decr
[eva] Recording results for apply
[eva] Done for function apply
[eva] calls_annotation.i:80: Reusing old results for call to incr
[eva] calls_annotation.i:82: Reusing old results for call to incr
[eva] computing for function square <- main.
Called from calls_annotation.i:85.
[eva] Recording results for square
[eva] Done for function square
[eva] computing for function decr <- main.
Called from calls_annotation.i:85.
[eva] Recording results for decr
[eva] Done for function decr
[eva] calls_annotation.i:85: Reusing old results for call to incr
[eva] computing for function square <- main.
Called from calls_annotation.i:88.
[eva] Recording results for square
[eva] Done for function square
[eva] computing for function apply <- main.
Called from calls_annotation.i:92.
[eva] computing for function square <- apply <- main.
Called from calls_annotation.i:38.
[eva] Recording results for square
[eva] Done for function square
[eva] computing for function square <- apply <- main.
Called from calls_annotation.i:40.
[eva] Recording results for square
[eva] Done for function square
[eva] Recording results for apply
[eva] Done for function apply
[eva] calls_annotation.i:80: Reusing old results for call to incr
[eva] calls_annotation.i:82: Reusing old results for call to decr
[eva:alarm] calls_annotation.i:85: Warning: calls annotation got status unknown.
[eva] calls_annotation.i:85: Reusing old results for call to square
[eva] calls_annotation.i:85: Reusing old results for call to decr
[eva] calls_annotation.i:85: Reusing old results for call to incr
[eva:alarm] calls_annotation.i:88: Warning:
calls annotation got status invalid (stopping propagation).
[eva] computing for function apply <- main.
Called from calls_annotation.i:92.
[eva:alarm] calls_annotation.i:38: Warning:
calls annotation got status invalid (stopping propagation).
[eva] Recording results for apply
[eva] Done for function apply
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function decr:
__retres ∈ {-4; -3; -2; -1; 0; 1}
[eva:final-states] Values at end of function incr:
__retres ∈ {-1; 0; 1; 2; 3; 4; 5; 6}
[eva:final-states] Values at end of function square:
__retres ∈ [-1..65536]
[eva:final-states] Values at end of function apply:
x ∈ [-4..65536]
[eva:final-states] Values at end of function main:
a ∈ {-1; 0; 1}
i ∈ {0; 1; 2}
[from] Computing for function decr
[from] Done for function decr
[from] Computing for function incr
[from] Done for function incr
[from] Computing for function square
[from] Done for function square
[from] Computing for function apply
[from] Computing for function error <-apply
[from] Non-terminating function error (no dependencies)
[from] Done for function error
[from] Done for function apply
[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 decr:
\result FROM x
[from] Function incr:
\result FROM x
[from] Function square:
\result FROM x
[from] Function apply:
\result FROM fp; a
[from] Function main:
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function decr:
__retres
[inout] Inputs for function decr:
\nothing
[inout] Out (internal) for function incr:
__retres
[inout] Inputs for function incr:
\nothing
[inout] Out (internal) for function square:
__retres
[inout] Inputs for function square:
\nothing
[inout] Out (internal) for function apply:
x
[inout] Inputs for function apply:
\nothing
[inout] Out (internal) for function main:
a; i; j
[inout] Inputs for function main:
nondet; funs[0..3]
tests/value/oracle_apron/calls_annotation.res.oracle 0 → 100644
+ 81
− 0
View file @ 8a310a69
57c57,60
< [eva] calls_annotation.i:80: Reusing old results for call to incr
---
> [eva] computing for function incr <- main.
> Called from calls_annotation.i:80.
> [eva] Recording results for incr
> [eva] Done for function incr
89,92c92,107
< [eva] calls_annotation.i:80: Reusing old results for call to incr
< [eva] calls_annotation.i:82: Reusing old results for call to decr
< [eva] calls_annotation.i:85: Reusing old results for call to decr
< [eva] calls_annotation.i:85: Reusing old results for call to incr
---
> [eva] computing for function incr <- main.
> Called from calls_annotation.i:80.
> [eva] Recording results for incr
> [eva] Done for function incr
> [eva] computing for function decr <- main.
> Called from calls_annotation.i:82.
> [eva] Recording results for decr
> [eva] Done for function decr
> [eva] computing for function decr <- main.
> Called from calls_annotation.i:85.
> [eva] Recording results for decr
> [eva] Done for function decr
> [eva] computing for function incr <- main.
> Called from calls_annotation.i:85.
> [eva] Recording results for incr
> [eva] Done for function incr
109,110c124,131
< [eva] calls_annotation.i:80: Reusing old results for call to incr
< [eva] calls_annotation.i:82: Reusing old results for call to incr
---
> [eva] computing for function incr <- main.
> Called from calls_annotation.i:80.
> [eva] Recording results for incr
> [eva] Done for function incr
> [eva] computing for function incr <- main.
> Called from calls_annotation.i:82.
> [eva] Recording results for incr
> [eva] Done for function incr
119c140,143
< [eva] calls_annotation.i:85: Reusing old results for call to incr
---
> [eva] computing for function incr <- main.
> Called from calls_annotation.i:85.
> [eva] Recording results for incr
> [eva] Done for function incr
136,137c160,167
< [eva] calls_annotation.i:80: Reusing old results for call to incr
< [eva] calls_annotation.i:82: Reusing old results for call to decr
---
> [eva] computing for function incr <- main.
> Called from calls_annotation.i:80.
> [eva] Recording results for incr
> [eva] Done for function incr
> [eva] computing for function decr <- main.
> Called from calls_annotation.i:82.
> [eva] Recording results for decr
> [eva] Done for function decr
139,141c169,180
< [eva] calls_annotation.i:85: Reusing old results for call to square
< [eva] calls_annotation.i:85: Reusing old results for call to decr
< [eva] calls_annotation.i:85: Reusing old results for call to incr
---
> [eva] computing for function square <- main.
> Called from calls_annotation.i:85.
> [eva] Recording results for square
> [eva] Done for function square
> [eva] computing for function decr <- main.
> Called from calls_annotation.i:85.
> [eva] Recording results for decr
> [eva] Done for function decr
> [eva] computing for function incr <- main.
> Called from calls_annotation.i:85.
> [eva] Recording results for incr
> [eva] Done for function incr
158c197
< __retres ∈ [-1..65536]
---
> __retres ∈ [0..65536]
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment