[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

@@ -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

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

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