From 10560989b33a1d5e03f68df48f1688185d73883f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 21 Nov 2019 13:21:52 +0100
Subject: [PATCH] [Eva] Adds a test of the summary when using both RTE and Eva.
---
tests/value/oracle/summary.0.res.oracle | 2 +-
tests/value/oracle/summary.2.res.oracle | 4 +-
tests/value/oracle/summary.3.res.oracle | 46 ++++----
tests/value/oracle/summary.4.res.oracle | 141 ++++++++++++++++++++++++
tests/value/summary.i | 1 +
5 files changed, 168 insertions(+), 26 deletions(-)
create mode 100644 tests/value/oracle/summary.4.res.oracle
diff --git a/tests/value/oracle/summary.0.res.oracle b/tests/value/oracle/summary.0.res.oracle
index fe68cdf367b..e8a24300ea5 100644
--- a/tests/value/oracle/summary.0.res.oracle
+++ b/tests/value/oracle/summary.0.res.oracle
@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization
undet ∈ [--..--]
volatile_d ∈ [--..--]
-[kernel:annot:missing-spec] tests/value/summary.i:18: Warning:
+[kernel:annot:missing-spec] tests/value/summary.i:19: Warning:
Neither code nor specification for function minimalist, generating default assigns from the prototype
[eva] using specification for function minimalist
[eva] done for function minimalist
diff --git a/tests/value/oracle/summary.2.res.oracle b/tests/value/oracle/summary.2.res.oracle
index 642453d6393..a45ac0df3bf 100644
--- a/tests/value/oracle/summary.2.res.oracle
+++ b/tests/value/oracle/summary.2.res.oracle
@@ -5,10 +5,10 @@
[eva:initial-state] Values of globals at initialization
undet ∈ [--..--]
volatile_d ∈ [--..--]
-[eva:alarm] tests/value/summary.i:14: Warning: division by zero. assert 0 ≢ 0;
+[eva:alarm] tests/value/summary.i:15: Warning: division by zero. assert 0 ≢ 0;
[eva] Recording results for bottom
[eva] done for function bottom
-[eva] tests/value/summary.i:14:
+[eva] tests/value/summary.i:15:
assertion 'Eva,division_by_zero' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function bottom:
diff --git a/tests/value/oracle/summary.3.res.oracle b/tests/value/oracle/summary.3.res.oracle
index 800aa84f7f4..d59ad1e10e2 100644
--- a/tests/value/oracle/summary.3.res.oracle
+++ b/tests/value/oracle/summary.3.res.oracle
@@ -6,56 +6,56 @@
undet ∈ [--..--]
volatile_d ∈ [--..--]
[eva] computing for function alarms <- main.
- Called from tests/value/summary.i:52.
-[eva:alarm] tests/value/summary.i:26: Warning:
+ Called from tests/value/summary.i:53.
+[eva:alarm] tests/value/summary.i:27: Warning:
out of bounds read. assert \valid_read(p);
-[eva:alarm] tests/value/summary.i:28: Warning:
- out of bounds write. assert \valid(p);
[eva:alarm] tests/value/summary.i:29: Warning:
+ out of bounds write. assert \valid(p);
+[eva:alarm] tests/value/summary.i:30: Warning:
accessing out of bounds index. assert 0 ≤ undet;
-[eva:alarm] tests/value/summary.i:29: Warning:
- accessing out of bounds index. assert undet < 10;
[eva:alarm] tests/value/summary.i:30: Warning:
- division by zero. assert undet ≢ 0;
+ accessing out of bounds index. assert undet < 10;
[eva:alarm] tests/value/summary.i:31: Warning:
+ division by zero. assert undet ≢ 0;
+[eva:alarm] tests/value/summary.i:32: Warning:
signed overflow. assert -2147483648 ≤ undet + undet;
-[eva:alarm] tests/value/summary.i:31: Warning:
- signed overflow. assert undet + undet ≤ 2147483647;
[eva:alarm] tests/value/summary.i:32: Warning:
+ signed overflow. assert undet + undet ≤ 2147483647;
+[eva:alarm] tests/value/summary.i:33: Warning:
invalid LHS operand for left shift. assert 0 ≤ undet;
-[eva:alarm] tests/value/summary.i:32: Warning:
+[eva:alarm] tests/value/summary.i:33: Warning:
invalid RHS operand for shift. assert 0 ≤ undet < 32;
-[eva:alarm] tests/value/summary.i:32: Warning:
- signed overflow. assert undet << undet ≤ 2147483647;
[eva:alarm] tests/value/summary.i:33: Warning:
- non-finite double value. assert \is_finite(volatile_d);
+ signed overflow. assert undet << undet ≤ 2147483647;
[eva:alarm] tests/value/summary.i:34: Warning:
- non-finite double value. assert \is_finite((double)(d - d));
+ non-finite double value. assert \is_finite(volatile_d);
[eva:alarm] tests/value/summary.i:35: Warning:
+ non-finite double value. assert \is_finite((double)(d - d));
+[eva:alarm] tests/value/summary.i:36: Warning:
overflow in conversion from floating-point to integer.
assert -2147483649 < d;
-[eva:alarm] tests/value/summary.i:35: Warning:
+[eva:alarm] tests/value/summary.i:36: Warning:
overflow in conversion from floating-point to integer. assert d < 2147483648;
-[eva:alarm] tests/value/summary.i:38: Warning:
- pointer subtraction. assert \base_addr(p) ≡ \base_addr(q);
[eva:alarm] tests/value/summary.i:39: Warning:
+ pointer subtraction. assert \base_addr(p) ≡ \base_addr(q);
+[eva:alarm] tests/value/summary.i:40: Warning:
pointer comparison. assert \pointer_comparable((void *)p, (void *)q);
-[eva:locals-escaping] tests/value/summary.i:42: Warning:
+[eva:locals-escaping] tests/value/summary.i:43: Warning:
locals {z} escaping the scope of a block of alarms through p
-[eva:alarm] tests/value/summary.i:44: Warning:
+[eva:alarm] tests/value/summary.i:45: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&p);
[eva] Recording results for alarms
[eva] Done for function alarms
[eva] computing for function f <- main.
- Called from tests/value/summary.i:53.
-[kernel:annot:missing-spec] tests/value/summary.i:53: Warning:
+ Called from tests/value/summary.i:54.
+[kernel:annot:missing-spec] tests/value/summary.i:54: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
[eva] using specification for function f
[eva] Done for function f
[eva] computing for function g <- main.
- Called from tests/value/summary.i:54.
-[kernel:annot:missing-spec] tests/value/summary.i:54: Warning:
+ Called from tests/value/summary.i:55.
+[kernel:annot:missing-spec] tests/value/summary.i:55: Warning:
Neither code nor specification for function g, generating default assigns from the prototype
[eva] using specification for function g
[eva] Done for function g
diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle
new file mode 100644
index 00000000000..507036d92ab
--- /dev/null
+++ b/tests/value/oracle/summary.4.res.oracle
@@ -0,0 +1,141 @@
+[kernel] Parsing tests/value/summary.i (no preprocessing)
+[rte] annotating function alarms
+[rte] annotating function bottom
+[rte] tests/value/summary.i:15: Warning:
+ guaranteed RTE: assert division_by_zero: 0 ≢ 0;
+[rte] annotating function main
+[rte] annotating function minimal
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ undet ∈ [--..--]
+ volatile_d ∈ [--..--]
+[eva] computing for function alarms <- main.
+ Called from tests/value/summary.i:53.
+[eva:alarm] tests/value/summary.i:27: Warning:
+ assertion 'rte,mem_access' got status unknown.
+[eva:alarm] tests/value/summary.i:29: Warning:
+ assertion 'rte,mem_access' got status unknown.
+[eva:alarm] tests/value/summary.i:30: Warning:
+ assertion 'rte,index_bound' got status unknown.
+[eva:alarm] tests/value/summary.i:30: Warning:
+ accessing out of bounds index. assert 0 ≤ undet;
+[eva:alarm] tests/value/summary.i:30: Warning:
+ accessing out of bounds index. assert undet < 10;
+[eva:alarm] tests/value/summary.i:31: Warning:
+ assertion 'rte,division_by_zero' got status unknown.
+[eva:alarm] tests/value/summary.i:31: Warning:
+ division by zero. assert undet ≢ 0;
+[eva:alarm] tests/value/summary.i:32: Warning:
+ assertion 'rte,signed_overflow' got status unknown.
+[eva:alarm] tests/value/summary.i:32: Warning:
+ signed overflow. assert -2147483648 ≤ undet + undet;
+[eva:alarm] tests/value/summary.i:32: Warning:
+ signed overflow. assert undet + undet ≤ 2147483647;
+[eva:alarm] tests/value/summary.i:33: Warning:
+ assertion 'rte,shift' got status unknown.
+[eva:alarm] tests/value/summary.i:33: Warning:
+ assertion 'rte,shift' got status unknown.
+[eva:alarm] tests/value/summary.i:33: Warning:
+ assertion 'rte,signed_overflow' got status unknown.
+[eva:alarm] tests/value/summary.i:33: Warning:
+ invalid LHS operand for left shift. assert 0 ≤ undet;
+[eva:alarm] tests/value/summary.i:33: Warning:
+ invalid RHS operand for shift. assert 0 ≤ undet < 32;
+[eva:alarm] tests/value/summary.i:33: Warning:
+ signed overflow. assert undet << undet ≤ 2147483647;
+[eva:alarm] tests/value/summary.i:34: Warning:
+ non-finite double value. assert \is_finite(volatile_d);
+[eva:alarm] tests/value/summary.i:35: Warning:
+ assertion 'rte,is_nan_or_infinite' got status unknown.
+[eva:alarm] tests/value/summary.i:35: Warning:
+ non-finite double value. assert \is_finite((double)(d - d));
+[eva:alarm] tests/value/summary.i:36: Warning:
+ assertion 'rte,float_to_int' got status unknown.
+[eva:alarm] tests/value/summary.i:39: Warning:
+ pointer subtraction. assert \base_addr(p) ≡ \base_addr(q);
+[eva:alarm] tests/value/summary.i:40: Warning:
+ pointer comparison. assert \pointer_comparable((void *)p, (void *)q);
+[eva:locals-escaping] tests/value/summary.i:43: Warning:
+ locals {z} escaping the scope of a block of alarms through p
+[eva:alarm] tests/value/summary.i:45: Warning:
+ assertion 'rte,mem_access' got status unknown.
+[eva:alarm] tests/value/summary.i:45: Warning:
+ accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&p);
+[eva] Recording results for alarms
+[eva] Done for function alarms
+[eva] computing for function f <- main.
+ Called from tests/value/summary.i:54.
+[kernel:annot:missing-spec] tests/value/summary.i:54: Warning:
+ Neither code nor specification for function f, generating default assigns from the prototype
+[eva] using specification for function f
+[eva] Done for function f
+[eva] computing for function g <- main.
+ Called from tests/value/summary.i:55.
+[kernel:annot:missing-spec] tests/value/summary.i:55: Warning:
+ Neither code nor specification for function g, generating default assigns from the prototype
+[eva] using specification for function g
+[eva] Done for function g
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function alarms:
+ x ∈ [--..--]
+ y ∈ {0}
+ p ∈ {{ &x ; &y }}
+ q ∈ {{ &x ; &y }}
+ t[0..9] ∈ {0}
+ d ∈ [-2147483649. .. 2147483648.]
+[eva:final-states] Values at end of function main:
+
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 4): 50% coverage.
+ In these functions, 32 statements reached (out of 32): 100% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 1 warning
+ by the Frama-C kernel: 0 errors 2 warnings
+ ----------------------------------------------------------------------------
+ 18 alarms generated by the analysis:
+ 1 division by zero
+ 3 invalid memory accesses
+ 2 accesses out of bounds index
+ 3 integer overflows
+ 2 invalid shifts
+ 1 escaping address
+ 2 nan or infinite floating-point values
+ 2 illegal conversions from floating-point to integer
+ 2 others
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[from] Computing for function alarms
+[from] Done for function alarms
+[from] Computing for function main
+[from] Computing for function f <-main
+[from] Done for function f
+[from] Computing for function g <-main
+[from] Done for function g
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function alarms:
+ NO EFFECTS
+[from] Function f:
+ NO EFFECTS
+[from] Function g:
+ NO EFFECTS
+[from] Function main:
+ NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function alarms:
+ x; y; p; q; t[0..9]; d
+[inout] Inputs for function alarms:
+ undet; volatile_d
+[inout] Out (internal) for function main:
+ \nothing
+[inout] Inputs for function main:
+ undet; volatile_d
diff --git a/tests/value/summary.i b/tests/value/summary.i
index b037fa17050..96ea72f491b 100644
--- a/tests/value/summary.i
+++ b/tests/value/summary.i
@@ -3,6 +3,7 @@
STDOPT: +"-eva-msg-key=summary -main minimal"
STDOPT: +"-eva-msg-key=summary -main bottom"
STDOPT: +"-eva-msg-key=summary -main main"
+ STDOPT: +"-rte -eva-msg-key=summary -main main"
*/
/* Tests the summary on the smallest possible program. */
--
GitLab