[Eva] Removes file register.ml; registers the analysis in analysis.ml.

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

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. *)

src/plugins/eva/register.ml

-(**************************************************************************)
-(*                                                                        *)
-(*  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:
-*)

src/plugins/eva/register.mli

-(**************************************************************************)
-(*                                                                        *)
-(*  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}. *)