From 602f15e9584ddd417644110d0646345630c217da Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 27 Jul 2023 15:51:27 +0200
Subject: [PATCH] [Eva] Removes file register.ml; registers the analysis in
analysis.ml.
---
src/plugins/eva/engine/analysis.ml | 22 ++++++++++++----
src/plugins/eva/engine/analysis.mli | 3 ---
src/plugins/eva/register.ml | 40 -----------------------------
src/plugins/eva/register.mli | 23 -----------------
4 files changed, 17 insertions(+), 71 deletions(-)
delete mode 100644 src/plugins/eva/register.ml
delete mode 100644 src/plugins/eva/register.mli
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index a93c6903e27..6bbfef27ba4 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -187,6 +187,8 @@ let cvalue_initial_state () =
let _, lib_entry = Globals.entry_point () in
G.get_cvalue_or_bottom (A.initial_state ~lib_entry)
+let () = Db.Value.initial_state_only_globals := cvalue_initial_state
+
(* Builds the Analyzer module corresponding to a given configuration,
and sets it as the current analyzer. *)
let make_analyzer config =
@@ -207,6 +209,12 @@ let reset_analyzer () =
if not (Abstractions.Config.equal config (fst !ref_analyzer))
then make_analyzer config
+(* Resets the Analyzer when the current project is changed. *)
+let () =
+ Project.register_after_set_current_hook
+ ~user_only:true (fun _ -> reset_analyzer ());
+ Project.register_after_global_load_hook reset_analyzer
+
(* Builds the analyzer if needed, and run the analysis. *)
let force_compute () =
Ast.compute ();
@@ -230,8 +238,12 @@ let compute =
let name = "Eva.Analysis.compute" in
fst (State_builder.apply_once name [ Self.state ] compute)
-(* Resets the Analyzer when the current project is changed. *)
-let () =
- Project.register_after_set_current_hook
- ~user_only:true (fun _ -> reset_analyzer ());
- Project.register_after_global_load_hook reset_analyzer
+let () = Db.Value.compute := 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 () = Db.Main.extend main
diff --git a/src/plugins/eva/engine/analysis.mli b/src/plugins/eva/engine/analysis.mli
index 8dd74f365d0..fe482f514af 100644
--- a/src/plugins/eva/engine/analysis.mli
+++ b/src/plugins/eva/engine/analysis.mli
@@ -154,6 +154,3 @@ val use_spec_instead_of_definition: Cil_types.kernel_function -> bool
to known whether results are available for a given function. *)
val save_results: Cil_types.kernel_function -> bool
[@@@ api_end]
-
-val cvalue_initial_state: unit -> Cvalue.Model.t
-(** Return the initial state of the cvalue domain only. *)
diff --git a/src/plugins/eva/register.ml b/src/plugins/eva/register.ml
deleted file mode 100644
index ea9d5774fbc..00000000000
--- a/src/plugins/eva/register.ml
+++ /dev/null
@@ -1,40 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-let () = Db.Value.compute := Analysis.compute
-let () = Parameters.ForceValues.set_output_dependencies [Self.state]
-
-let main () =
- (* Value computations *)
- if Parameters.ForceValues.get () then Analysis.compute ();
- if Analysis.is_computed () then Red_statuses.report ()
-
-let () = Db.Main.extend main
-
-let () = Db.Value.initial_state_only_globals := Analysis.cvalue_initial_state
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/plugins/eva/register.mli b/src/plugins/eva/register.mli
deleted file mode 100644
index 692074101d4..00000000000
--- a/src/plugins/eva/register.mli
+++ /dev/null
@@ -1,23 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(** Functions of the Value plugin registered in {!Db}. *)
--
GitLab