diff --git a/src/plugins/value/utils/value_results.ml b/src/plugins/value/utils/value_results.ml
index 4363193a1b51f6a8de4275dde0e0a23aa1f4434e..d82bc2853b2e0ab84a0d2998efa46bbfa702b833 100644
--- a/src/plugins/value/utils/value_results.ml
+++ b/src/plugins/value/utils/value_results.ml
@@ -498,7 +498,8 @@ let make_report () =
let report = empty_report () in
let report_property ip =
match ip with
- | Property.IPCodeAnnot {Property.ica_ca} ->
+ | Property.IPCodeAnnot Property.{ ica_ca; ica_stmt; }
+ when Db.Value.is_reachable_stmt ica_stmt ->
begin
let status = get_status ip in
match Alarms.find ica_ca with
@@ -506,11 +507,13 @@ let make_report () =
| Some alarm ->
let acc_status, acc_alarms = report.alarms in
report_status acc_status status;
- report_alarm acc_alarms alarm
+ match status with
+ | None | Some Property_status.True -> ()
+ | _ -> report_alarm acc_alarms alarm
end
- | Property.IPPropertyInstance _ ->
- let status = get_status ip in
- report_status report.preconds status
+ | Property.IPPropertyInstance {Property.ii_stmt}
+ when Db.Value.is_reachable_stmt ii_stmt ->
+ report_status report.preconds (get_status ip)
| _ -> ()
in
Property_status.iter report_property;
diff --git a/tests/journal/oracle/intra.res.oracle b/tests/journal/oracle/intra.res.oracle
index 9032dd6f7aef8be7a8e414890d3e99b037adf17d..2685f39927be4bd34322f4a498a8a0ab31ea3cb3 100644
--- a/tests/journal/oracle/intra.res.oracle
+++ b/tests/journal/oracle/intra.res.oracle
@@ -68,7 +68,7 @@
0 alarms generated by the analysis.
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
- Assertions 6 valid 0 unknown 0 invalid 6 total
+ Assertions 4 valid 0 unknown 0 invalid 4 total
Preconditions 0 valid 0 unknown 0 invalid 0 total
100% of the logical properties reached have been proven.
----------------------------------------------------------------------------
diff --git a/tests/misc/oracle/bts1201.res.oracle b/tests/misc/oracle/bts1201.res.oracle
index b15cb77c71ad3712d598439a18afb2b5be94afb6..5d683d1decf911024bb296418d7fb0ea6661b50a 100644
--- a/tests/misc/oracle/bts1201.res.oracle
+++ b/tests/misc/oracle/bts1201.res.oracle
@@ -35,10 +35,7 @@
----------------------------------------------------------------------------
0 alarms generated by the analysis.
----------------------------------------------------------------------------
- Evaluation of the logical properties reached by the analysis:
- Assertions 1 valid 0 unknown 0 invalid 1 total
- Preconditions 0 valid 0 unknown 0 invalid 0 total
- 100% of the logical properties reached have been proven.
+ No logical properties have been reached by the analysis.
----------------------------------------------------------------------------
/* Generated by Frama-C */
void main(void)
diff --git a/tests/value/oracle/summary.0.res.oracle b/tests/value/oracle/summary.0.res.oracle
index fe68cdf367b9ebc43d0a69b2de88ec79fd1a6378..3229f4ccf36d2a7a4b4b2c647a5d7f5da54cae4c 100644
--- a/tests/value/oracle/summary.0.res.oracle
+++ b/tests/value/oracle/summary.0.res.oracle
@@ -5,14 +5,14 @@
[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
[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 c3d37ddacc8540eb714fae0b9b041752aa5a0383..22e89c6c41bc3cc3fd942cfb5ac9836f43a89723 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 642453d63930e4727c5d6ac5f842e6f7657f2cce..eab565f4a312fca620dc19315fa9aab51302b240 100644
--- a/tests/value/oracle/summary.2.res.oracle
+++ b/tests/value/oracle/summary.2.res.oracle
@@ -5,17 +5,17 @@
[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:
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 800aa84f7f444f248e282ca4458e5872cd1cea8b..f5bcadc1abb5d0f1908434ef0ff16c53d5cdbe34 100644
--- a/tests/value/oracle/summary.3.res.oracle
+++ b/tests/value/oracle/summary.3.res.oracle
@@ -6,56 +6,64 @@
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:62.
+[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 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:53.
-[kernel:annot:missing-spec] tests/value/summary.i:53: 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:54.
-[kernel:annot:missing-spec] tests/value/summary.i:54: 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
new file mode 100644
index 0000000000000000000000000000000000000000..80d3ffdb4b19723e3faea13031852ffe5fbcb15e
--- /dev/null
+++ b/tests/value/oracle/summary.4.res.oracle
@@ -0,0 +1,164 @@
+[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 dead
+[rte] annotating function logic
+[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:62.
+[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 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: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: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
+[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 logic:
+
+[eva:final-states] Values at end of function main:
+
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 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
+ 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
+ ----------------------------------------------------------------------------
+ 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
+[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 logic:
+ 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 logic:
+ \nothing
+[inout] Inputs for function logic:
+ undet
+[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 b037fa17050b083cf6758ef68c9579ea5223544e..d73b4b42d73532f315dedb80d1c927415566d9eb 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. */
@@ -47,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; */
+}