diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml index f63494c9e5bc801138d2e7eff89d2d5b4bab28ab..1fcd2719a6da58bb0e18f9d222dd10cae7b3a1e1 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 fedba296eddd9005f0397515a5791347f3ebb2e5..80b2ad866a91af29903f834b106b43b31eb93424 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 bdad22b9a665902718fc25051c5444a0ff1482ad..01af779f31d48018f83d623336724334b696bbfd 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