From fb62c8fa8568afa48ca97ca16b178be5ff6cad6e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 25 Nov 2019 10:55:00 +0100
Subject: [PATCH] [Eva] In the summary, do not count unreachable logical
properties as proven.
---
src/plugins/value/utils/value_results.ml | 9 +++++----
tests/journal/oracle/intra.res.oracle | 2 +-
tests/misc/oracle/bts1201.res.oracle | 5 +----
3 files changed, 7 insertions(+), 9 deletions(-)
diff --git a/src/plugins/value/utils/value_results.ml b/src/plugins/value/utils/value_results.ml
index 8cc88aceefd..d82bc2853b2 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
@@ -510,9 +511,9 @@ let make_report () =
| 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 9032dd6f7ae..2685f39927b 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 b15cb77c71a..5d683d1decf 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)
--
GitLab