From b841e3db71595283d23c54548fc682ee49d0b125 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 23 Apr 2024 21:06:23 +0200
Subject: [PATCH] [Eva] Reports red statuses in post_analysis, and not in the
main function.
Thus, red statuses are only reported at the end of an analysis.
---
src/plugins/eva/engine/analysis.ml | 6 +-----
src/plugins/eva/engine/compute_functions.ml | 3 ++-
tests/value/oracle/red_alarms.res.oracle | 2 +-
3 files changed, 4 insertions(+), 7 deletions(-)
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index f63494c9e5b..1fcd2719a6d 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -231,9 +231,5 @@ let compute =
let () = Parameters.ForceValues.set_output_dependencies [Self.state]
-let main () =
- (* Value computations *)
- if Parameters.ForceValues.get () then compute ();
- if is_computed () then Red_statuses.report ()
-
+let main () = if Parameters.ForceValues.get () then compute ()
let () = Boot.Main.extend main
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index fedba296edd..80b2ad866a9 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -127,7 +127,8 @@ let post_analysis () =
Eva_dynamic.RteGen.mark_generated_rte ();
post_analysis_cleanup ~aborted:false;
(* Remove redundant alarms *)
- if Parameters.RmAssert.get () then Eva_dynamic.Scope.rm_asserts ()
+ if Parameters.RmAssert.get () then Eva_dynamic.Scope.rm_asserts ();
+ Red_statuses.report ()
(* Registers signal handlers for SIGUSR1 and SIGINT to cleanly abort the Eva
analysis. Returns a function that restores previous signal behaviors after
diff --git a/tests/value/oracle/red_alarms.res.oracle b/tests/value/oracle/red_alarms.res.oracle
index bdad22b9a66..01af779f31d 100644
--- a/tests/value/oracle/red_alarms.res.oracle
+++ b/tests/value/oracle/red_alarms.res.oracle
@@ -112,6 +112,7 @@
[eva] Recording results for main
[eva] Done for function main
[eva] red_alarms.i:45: assertion 'Eva,index_bound' got final status invalid.
+[eva] Listing red statuses in file red_alarms.csv
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function in_bound:
y ∈ [0..99]
@@ -136,7 +137,6 @@
x ∈ [--..--]
[eva:final-states] Values at end of function main:
-[eva] Listing red statuses in file red_alarms.csv
[from] Computing for function in_bound
[from] Done for function in_bound
[from] Computing for function maybe_swap
--
GitLab