From 8a310a69eaa5ce2b48357428a0da44224ad3cbc3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 2 Aug 2024 16:42:25 +0200
Subject: [PATCH] [Eva] Adds a test for the evaluation of "calls" annotations.
---
tests/value/calls_annotation.i | 101 +++++++++
.../value/oracle/calls_annotation.res.oracle | 209 ++++++++++++++++++
.../oracle_apron/calls_annotation.res.oracle | 81 +++++++
3 files changed, 391 insertions(+)
create mode 100644 tests/value/calls_annotation.i
create mode 100644 tests/value/oracle/calls_annotation.res.oracle
create mode 100644 tests/value/oracle_apron/calls_annotation.res.oracle
diff --git a/tests/value/calls_annotation.i b/tests/value/calls_annotation.i
new file mode 100644
index 00000000000..3a9b799aa1d
--- /dev/null
+++ b/tests/value/calls_annotation.i
@@ -0,0 +1,101 @@
+/* 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);
+ }
+ }
+}
diff --git a/tests/value/oracle/calls_annotation.res.oracle b/tests/value/oracle/calls_annotation.res.oracle
new file mode 100644
index 00000000000..e22c92eeaa0
--- /dev/null
+++ b/tests/value/oracle/calls_annotation.res.oracle
@@ -0,0 +1,209 @@
+[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]
diff --git a/tests/value/oracle_apron/calls_annotation.res.oracle b/tests/value/oracle_apron/calls_annotation.res.oracle
new file mode 100644
index 00000000000..2b7f3f96a5e
--- /dev/null
+++ b/tests/value/oracle_apron/calls_annotation.res.oracle
@@ -0,0 +1,81 @@
+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]
--
GitLab