From c1a114d8a95a3d528029bd66d96374d77adac0d6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 16 Jul 2024 16:14:35 +0200
Subject: [PATCH] [Eva] Fixes count of sure alarms by function.
Status of emitted alarms can be changed to valid/invalid at the end of the
analysis. We thus need to recompute statistics for all analyzed functions.
---
src/plugins/eva/engine/compute_functions.ml | 2 ++
src/plugins/eva/utils/summary.ml | 14 +++++++++-----
src/plugins/eva/utils/summary.mli | 6 +++---
3 files changed, 14 insertions(+), 8 deletions(-)
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 80b2ad866a9..e853b106bab 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -128,6 +128,8 @@ let post_analysis () =
post_analysis_cleanup ~aborted:false;
(* Remove redundant alarms *)
if Parameters.RmAssert.get () then Eva_dynamic.Scope.rm_asserts ();
+ (* The above functions may have changed the status of alarms. *)
+ Summary.FunctionStats.recompute_all ();
Red_statuses.report ()
(* Registers signal handlers for SIGUSR1 and SIGINT to cleanly abort the Eva
diff --git a/src/plugins/eva/utils/summary.ml b/src/plugins/eva/utils/summary.ml
index db6f0b4e544..f975ac4ad1f 100644
--- a/src/plugins/eva/utils/summary.ml
+++ b/src/plugins/eva/utils/summary.ml
@@ -147,12 +147,18 @@ end
(* --- Function stats computation --- *)
+(* When Eva has emitted several statuses, keep the most precise. *)
+let merge_status acc new_status =
+ match acc, new_status with
+ | Some _, Property_status.Dont_know -> acc
+ | _ -> Some new_status
+
let get_status ip =
let eva_emitter = Eva_utils.emitter in
let aux_status emitter status acc =
let emitter = Emitter.Usable_emitter.get emitter.Property_status.emitter in
if Emitter.equal eva_emitter emitter
- then Some status
+ then merge_status acc status
else acc
in
Property_status.fold_on_statuses aux_status ip None
@@ -214,10 +220,8 @@ module FunctionStats = struct
let size = 17
end)
- let get kf =
- try Some (find kf)
- with Not_found -> None
let recompute kf = replace kf (compute_fun_stats kf)
+ let recompute_all () = iter (fun kf _ -> recompute kf)
end
@@ -284,7 +288,7 @@ let compute_stats () =
let do_fun fundec =
let kf = Globals.Functions.get fundec.Cil_types.svar in
let consider = consider_function fundec.Cil_types.svar in
- match FunctionStats.get kf with
+ match FunctionStats.find_opt kf with
| Some fun_stats ->
AlarmsStats.add_list prog_alarms fun_stats.fun_alarm_count;
if consider then
diff --git a/src/plugins/eva/utils/summary.mli b/src/plugins/eva/utils/summary.mli
index e434b9da54d..fbbbddd43ff 100644
--- a/src/plugins/eva/utils/summary.mli
+++ b/src/plugins/eva/utils/summary.mli
@@ -69,15 +69,15 @@ sig
type key = Kernel_function.t
type data = fun_stats
- (** Get the current analysis statistics for a function *)
- val get: key -> data option
-
(** Iterate on every function statistics *)
val iter: (key -> data -> unit) -> unit
(** Trigger the recomputation of function stats *)
val recompute: key -> unit
+ (* Trigger the recomputation of all function stats. *)
+ val recompute_all: unit -> unit
+
(** Set a hook on function statistics computation *)
val add_hook_on_change:
((key, data) State_builder.hashtbl_event -> unit) -> unit
--
GitLab