[eacsl] Move pre-analyses in a separate module

src/plugins/e-acsl/Makefile.in

@@ -71,7 +71,8 @@ SRC_ANALYSES:= \
 	typing \
 	literal_strings \
 	memory_tracking \
-	exit_points
+	exit_points \
+	analyses
 SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
 
 # code generator

src/plugins/e-acsl/headers/header_spec.txt

@@ -81,6 +81,8 @@ share/e-acsl/e_acsl.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 share/e-acsl/e_acsl_rtl.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/analyses_datatype.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/analyses_datatype.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/analyses.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/analyses.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/analyses_types.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/bound_variables.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/bound_variables.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL

src/plugins/e-acsl/src/analyses/analyses.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2021                                               *)
+(*    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 analyses_feedback msg =
+  Options.feedback ~level:2 "%s in %a" msg Project.pretty (Project.current ())
+
+let preprocess () =
+  let ast = Ast.get () in
+  analyses_feedback "preprocessing annotations";
+  Logic_normalizer.preprocess ast;
+  analyses_feedback "normalizing quantifiers";
+  Bound_variables.preprocess ast;
+  analyses_feedback "typing annotations";
+  Typing.type_program ast
+
+let reset () =
+  Memory_tracking.reset ();
+  Literal_strings.reset ();
+  Bound_variables.clear_guards ();
+  Logic_normalizer.clear ();
+  Typing.clear ()

src/plugins/e-acsl/src/analyses/analyses.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2021                                               *)
+(*    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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** General module for E-ACSL analyses *)
+
+val preprocess: unit -> unit
+(** Analyses to run before starting the translation *)
+
+val reset: unit -> unit
+(** Clear the results of the analyses *)

src/plugins/e-acsl/src/code_generator/injector.ml

@@ -840,13 +840,9 @@ let reset_all ast =
   (* by default, do not run E-ACSL on the generated code *)
   Options.Run.off ();
   (* reset all the E-ACSL environments to their original states *)
-  Memory_tracking.reset ();
   Logic_functions.reset ();
-  Literal_strings.reset ();
   Global_observer.reset ();
-  Bound_variables.clear_guards ();
-  Logic_normalizer.clear ();
-  Typing.clear ();
+  Analyses.reset ();
   (* reset some kernel states: *)
   (* reset the CFG that has been heavily modified by the code generation step *)
   Cfg.clearFileCFG ~clear_id:false ast;
@@ -856,23 +852,10 @@ let reset_all ast =
   Ast.mark_as_grown ()
 
 let inject () =
-  Gmp_types.init ();
   let ast = Ast.get () in
   let current_project = Project.current() in
   Options.feedback ~level:2
-    "preprocessing annotations in project %a"
-    Project.pretty current_project;
-  Logic_normalizer.preprocess ast;
-  Options.feedback ~level:2
-    "normalizing quantifiers in project %a"
-    Project.pretty current_project;
-  Bound_variables.preprocess ast;
-  Options.feedback ~level:2
-    "typing annotations in project %a"
-    Project.pretty current_project;
-  Typing.type_program ast;
-  Options.feedback ~level:2
-    "injecting annotations as code in project %a"
+    "injecting annotations as code in %a"
     Project.pretty current_project;
   inject_in_file ast;
   reset_all ast;

src/plugins/e-acsl/src/main.ml

@@ -69,7 +69,13 @@ let generate_code =
               Kernel.SignedOverflow.unsafe_set signed;
               Kernel.UnsignedOverflow.unsafe_set unsigned
             in
-            Extlib.try_finally ~finally Injector.inject ();
+            Extlib.try_finally
+              ~finally
+              (fun () ->
+                 Gmp_types.init ();
+                 Analyses.preprocess ();
+                 Injector.inject ())
+              ();
             (* remove the RTE's results computed from E-ACSL: they are partial
                and associated with the wrong kernel function (the one of the old
                project). *)