From 889fea20980eed5a111e56cfbb2e610b397bcb9f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 25 Nov 2019 11:08:24 +0100
Subject: [PATCH] [Eva] Adds a test of the summary of logical properties
evaluation.
---
tests/value/oracle/summary.0.res.oracle | 2 +-
tests/value/oracle/summary.1.res.oracle | 2 +-
tests/value/oracle/summary.2.res.oracle | 2 +-
tests/value/oracle/summary.3.res.oracle | 37 ++++++++++++++++++-----
tests/value/oracle/summary.4.res.oracle | 39 ++++++++++++++++++++-----
tests/value/summary.i | 16 ++++++++++
6 files changed, 79 insertions(+), 19 deletions(-)
diff --git a/tests/value/oracle/summary.0.res.oracle b/tests/value/oracle/summary.0.res.oracle
index e8a24300ea5..3229f4ccf36 100644
--- a/tests/value/oracle/summary.0.res.oracle
+++ b/tests/value/oracle/summary.0.res.oracle
@@ -12,7 +12,7 @@
[eva] ====== VALUES COMPUTED ======
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 0 functions analyzed (out of 4): 0% coverage.
+ 0 functions analyzed (out of 6): 0% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 0 warnings
diff --git a/tests/value/oracle/summary.1.res.oracle b/tests/value/oracle/summary.1.res.oracle
index c3d37ddacc8..22e89c6c41b 100644
--- a/tests/value/oracle/summary.1.res.oracle
+++ b/tests/value/oracle/summary.1.res.oracle
@@ -12,7 +12,7 @@
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 1 function analyzed (out of 4): 25% coverage.
+ 1 function analyzed (out of 6): 16% coverage.
In this function, 1 statements reached (out of 1): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
diff --git a/tests/value/oracle/summary.2.res.oracle b/tests/value/oracle/summary.2.res.oracle
index a45ac0df3bf..eab565f4a31 100644
--- a/tests/value/oracle/summary.2.res.oracle
+++ b/tests/value/oracle/summary.2.res.oracle
@@ -15,7 +15,7 @@
NON TERMINATING FUNCTION
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 1 function analyzed (out of 4): 25% coverage.
+ 1 function analyzed (out of 6): 16% coverage.
In this function, 1 statements reached (out of 2): 50% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
diff --git a/tests/value/oracle/summary.3.res.oracle b/tests/value/oracle/summary.3.res.oracle
index d59ad1e10e2..f5bcadc1abb 100644
--- a/tests/value/oracle/summary.3.res.oracle
+++ b/tests/value/oracle/summary.3.res.oracle
@@ -6,7 +6,7 @@
undet ∈ [--..--]
volatile_d ∈ [--..--]
[eva] computing for function alarms <- main.
- Called from tests/value/summary.i:53.
+ Called from tests/value/summary.i:62.
[eva:alarm] tests/value/summary.i:27: Warning:
out of bounds read. assert \valid_read(p);
[eva:alarm] tests/value/summary.i:29: Warning:
@@ -47,15 +47,23 @@
assert ¬\dangling(&p);
[eva] Recording results for alarms
[eva] Done for function alarms
+[eva] computing for function logic <- main.
+ Called from tests/value/summary.i:63.
+[eva] tests/value/summary.i:53: assertion got status valid.
+[eva:alarm] tests/value/summary.i:54: Warning: assertion got status unknown.
+[eva:alarm] tests/value/summary.i:56: Warning:
+ assertion got status invalid (stopping propagation).
+[eva] Recording results for logic
+[eva] Done for function logic
[eva] computing for function f <- main.
- Called from tests/value/summary.i:54.
-[kernel:annot:missing-spec] tests/value/summary.i:54: Warning:
+ Called from tests/value/summary.i:64.
+[kernel:annot:missing-spec] tests/value/summary.i:64: 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:
+ Called from tests/value/summary.i:65.
+[kernel:annot:missing-spec] tests/value/summary.i:65: 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
@@ -69,12 +77,14 @@
q ∈ {{ &x ; &y }}
t[0..9] ∈ {0}
d ∈ [-2147483649. .. 2147483648.]
+[eva:final-states] Values at end of function logic:
+
[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.
+ 3 functions analyzed (out of 6): 50% coverage.
+ In these functions, 38 statements reached (out of 38): 100% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 1 warning
@@ -91,10 +101,15 @@
2 illegal conversions from floating-point to integer
2 others
----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 1 valid 1 unknown 1 invalid 3 total
+ Preconditions 0 valid 0 unknown 0 invalid 0 total
+ 33% of the logical properties reached have been proven.
----------------------------------------------------------------------------
[from] Computing for function alarms
[from] Done for function alarms
+[from] Computing for function logic
+[from] Done for function logic
[from] Computing for function main
[from] Computing for function f <-main
[from] Done for function f
@@ -109,6 +124,8 @@
NO EFFECTS
[from] Function g:
NO EFFECTS
+[from] Function logic:
+ NO EFFECTS
[from] Function main:
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
@@ -116,6 +133,10 @@
x; y; p; q; t[0..9]; d
[inout] Inputs for function alarms:
undet; volatile_d
+[inout] Out (internal) for function logic:
+ \nothing
+[inout] Inputs for function logic:
+ undet
[inout] Out (internal) for function main:
\nothing
[inout] Inputs for function main:
diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle
index 507036d92ab..80d3ffdb4b1 100644
--- a/tests/value/oracle/summary.4.res.oracle
+++ b/tests/value/oracle/summary.4.res.oracle
@@ -3,6 +3,8 @@
[rte] annotating function bottom
[rte] tests/value/summary.i:15: Warning:
guaranteed RTE: assert division_by_zero: 0 ≢ 0;
+[rte] annotating function dead
+[rte] annotating function logic
[rte] annotating function main
[rte] annotating function minimal
[eva] Analyzing a complete application starting at main
@@ -12,7 +14,7 @@
undet ∈ [--..--]
volatile_d ∈ [--..--]
[eva] computing for function alarms <- main.
- Called from tests/value/summary.i:53.
+ Called from tests/value/summary.i:62.
[eva:alarm] tests/value/summary.i:27: Warning:
assertion 'rte,mem_access' got status unknown.
[eva:alarm] tests/value/summary.i:29: Warning:
@@ -66,15 +68,23 @@
assert ¬\dangling(&p);
[eva] Recording results for alarms
[eva] Done for function alarms
+[eva] computing for function logic <- main.
+ Called from tests/value/summary.i:63.
+[eva] tests/value/summary.i:53: assertion got status valid.
+[eva:alarm] tests/value/summary.i:54: Warning: assertion got status unknown.
+[eva:alarm] tests/value/summary.i:56: Warning:
+ assertion got status invalid (stopping propagation).
+[eva] Recording results for logic
+[eva] Done for function logic
[eva] computing for function f <- main.
- Called from tests/value/summary.i:54.
-[kernel:annot:missing-spec] tests/value/summary.i:54: Warning:
+ Called from tests/value/summary.i:64.
+[kernel:annot:missing-spec] tests/value/summary.i:64: 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:
+ Called from tests/value/summary.i:65.
+[kernel:annot:missing-spec] tests/value/summary.i:65: 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
@@ -88,12 +98,14 @@
q ∈ {{ &x ; &y }}
t[0..9] ∈ {0}
d ∈ [-2147483649. .. 2147483648.]
+[eva:final-states] Values at end of function logic:
+
[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.
+ 3 functions analyzed (out of 6): 50% coverage.
+ In these functions, 38 statements reached (out of 38): 100% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 1 warning
@@ -110,10 +122,15 @@
2 illegal conversions from floating-point to integer
2 others
----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 1 valid 1 unknown 1 invalid 3 total
+ Preconditions 0 valid 0 unknown 0 invalid 0 total
+ 33% of the logical properties reached have been proven.
----------------------------------------------------------------------------
[from] Computing for function alarms
[from] Done for function alarms
+[from] Computing for function logic
+[from] Done for function logic
[from] Computing for function main
[from] Computing for function f <-main
[from] Done for function f
@@ -128,6 +145,8 @@
NO EFFECTS
[from] Function g:
NO EFFECTS
+[from] Function logic:
+ NO EFFECTS
[from] Function main:
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
@@ -135,6 +154,10 @@
x; y; p; q; t[0..9]; d
[inout] Inputs for function alarms:
undet; volatile_d
+[inout] Out (internal) for function logic:
+ \nothing
+[inout] Inputs for function logic:
+ undet
[inout] Out (internal) for function main:
\nothing
[inout] Inputs for function main:
diff --git a/tests/value/summary.i b/tests/value/summary.i
index 96ea72f491b..d73b4b42d73 100644
--- a/tests/value/summary.i
+++ b/tests/value/summary.i
@@ -48,9 +48,25 @@ void alarms () {
void f(void);
void g(void);
+/* 1 valid assertion, 1 unknown assertion, 1 invalid assertion. */
+void logic () {
+ /*@ assert \true; */
+ /*@ assert undet == 0; */
+ if (undet)
+ /*@ assert \false; */
+ ;
+}
+
// 2 kernel warnings, 1 eva warning, no error.
void main () {
alarms ();
+ logic ();
f(); // kernel warning: no specification for function f
g(); // kernel warning: no specification for function g
}
+
+/* Assertions in this function should not appear in the summary. */
+void dead () {
+ /*@ assert \true; */
+ /*@ assert \false; */
+}
--
GitLab