[e-acsl] remove option -e-acsl-prepare

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

@@ -30,91 +30,6 @@ let check =
     (Datatype.func Datatype.unit Datatype.bool)
     check
 
-type extended_project =
-  | To_be_extended
-  | Already_extended of Project.t option (* None = keep the current project *)
-
-let extended_ast_project: extended_project ref = ref To_be_extended
-
-let unmemoized_extend_ast () =
-  let extend () =
-    let share = Options.Share.get_dir ~mode:`Must_exist "." in
-    Options.feedback ~level:3 "setting kernel options for E-ACSL.";
-    Kernel.CppExtraArgs.add
-      (Format.asprintf " -DE_ACSL_MACHDEP=%s -I%a/memory_model"
-         (Kernel.Machdep.get ())
-         Datatype.Filepath.pp_abs share);
-    Kernel.Keep_unused_specified_functions.off ();
-    if Plugin.is_present "variadic" then
-      Dynamic.Parameter.Bool.off "-variadic-translation" ();
-    let ppc, ppk = File.get_preprocessor_command () in
-    let register s =
-      File.pre_register
-        (File.NeedCPP
-           (s,
-            ppc
-            ^ Format.asprintf " -I%a" Datatype.Filepath.pp_abs share,
-            ppk))
-    in
-    List.iter register (Misc.library_files ())
-  in
-  if Ast.is_computed () then begin
-    (* do not modify the existing project: work on a copy.
-       Must also extend the current AST with the E-ACSL's library files. *)
-    Options.feedback ~level:2
-      "AST already computed: E-ACSL is going to work on a copy.";
-    let name = Project.get_name (Project.current ()) in
-    let tmpfile =
-      Extlib.temp_file_cleanup_at_exit ("e_acsl_" ^ name) ".i" in
-    let cout = open_out tmpfile in
-    let fmt = Format.formatter_of_out_channel cout in
-    File.pretty_ast ~fmt ();
-    let selection =
-      State_selection.diff
-        State_selection.full
-        (State_selection.with_dependencies Ast.self)
-    in
-    let prj =
-      Project.create_by_copy
-        ~last:false
-        ~selection
-        (Format.asprintf "%s for E-ACSL" name)
-    in
-    Project.on prj
-      (fun () ->
-         Kernel.Files.set [ Datatype.Filepath.of_string tmpfile ];
-         extend ())
-      ();
-    Some prj
-  end else begin
-    extend ();
-    None
-  end
-
-let extend_ast () = match !extended_ast_project with
-  | To_be_extended ->
-    let prj = unmemoized_extend_ast () in
-    extended_ast_project := Already_extended prj;
-    (match prj with
-     | None -> Project.current ()
-     | Some prj -> prj)
-  | Already_extended None ->
-    Project.current ()
-  | Already_extended(Some prj) ->
-    prj
-
-let apply_on_e_acsl_ast f x =
-  let tmp_prj = extend_ast () in
-  let res = Project.on tmp_prj f x in
-  (match !extended_ast_project with
-   | To_be_extended -> assert false
-   | Already_extended None -> ()
-   | Already_extended (Some prj) ->
-     assert (Project.equal prj tmp_prj);
-     extended_ast_project := To_be_extended;
-     if Options.Debug.get () = 0 then Project.remove ~project:tmp_prj ());
-  res
-
 module Resulting_projects =
   State_builder.Hashtbl
     (Datatype.String.Hashtbl)
@@ -133,32 +48,46 @@ let () =
 let generate_code =
   Resulting_projects.memo
     (fun name ->
-       apply_on_e_acsl_ast
+       Options.feedback "beginning translation.";
+       Temporal.enable (Options.Temporal_validity.get ());
+       let rtl_prj =
+         Project.create_by_copy ~last:false "E_ACSL RTL"
+       in
+       if Plugin.is_present "variadic" then begin
+         let opt_name = "-variadic-translation" in
+         if Dynamic.Parameter.Bool.get opt_name () then begin
+           if Ast.is_computed () then
+             Options.abort
+               "The variadic translation must be turned off for E-ACSL. \
+                Please use option '-variadic-no-translation'";
+           Options.warning "deactivating variadic translation";
+           Dynamic.Parameter.Bool.off opt_name ();
+         end
+       end;
+       Ast.compute ();
+       let copied_prj = Project.create_by_copy ~last:true name in
+       Project.on
+         copied_prj
          (fun () ->
-            Options.feedback "beginning translation.";
-            Temporal.enable (Options.Temporal_validity.get ());
-            let copied_prj =
-              Project.create_by_copy name ~last:true
+            (* preparation of the AST does not concern the E-ACSL RTL *)
+            Prepare_ast.prepare ();
+            Rtl.link rtl_prj;
+            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). *)
+            (* [TODO ARCHI] what if RTE was already computed? *)
+            let selection =
+              State_selection.union
+                (State_selection.with_dependencies !Db.RteGen.self)
+                (State_selection.with_dependencies Options.Run.self)
             in
-            Project.on
-              copied_prj
-              (fun () ->
-                 Prepare_ast.prepare ();
-                 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). *)
-                 (* [TODO ARCHI] what if RTE was already computed? *)
-                 let selection =
-                   State_selection.with_dependencies !Db.RteGen.self
-                 in
-                 Project.clear ~selection ~project:copied_prj ();
-                 Resulting_projects.mark_as_computed ())
-              ();
-            Options.feedback "translation done in project \"%s\"."
-              (Options.Project_name.get ());
-            copied_prj)
-         ())
+            Project.clear ~selection ~project:copied_prj ();
+            Resulting_projects.mark_as_computed ())
+         ();
+       Options.feedback "translation done in project \"%s\"."
+         (Options.Project_name.get ());
+       copied_prj)
 
 let generate_code =
   Dynamic.register
@@ -177,15 +106,6 @@ let predicate_to_exp =
        Kernel_function.ty Cil_datatype.Predicate.ty Cil_datatype.Exp.ty)
     Translate.predicate_to_exp
 
-let add_e_acsl_library _files =
-  if Options.must_visit () || Options.Prepare.get () then ignore (extend_ast ())
-
-(* extending the AST as soon as possible reduce the amount of time the AST is
-   duplicated:
-   - that is faster
-   - locations are better (indicate an existing file, and not a temp file) *)
-let () = Cmdline.run_after_configuring_stage add_e_acsl_library
-
 (* The Frama-C standard library contains specific built-in variables prefixed by
    "__fc_" and declared as extern: they prevent the generated code to be
    linked. This modification of the default printer replaces them by their
@@ -251,14 +171,12 @@ let main () =
   Keep_status.clear ();
   if Options.Run.get () then begin
     change_printer ();
-    ignore (generate_code (Options.Project_name.get ()))
+    ignore (generate_code (Options.Project_name.get ()));
   end else
-  if Options.Check.get () then
-    apply_on_e_acsl_ast
-      (fun () ->
-         Gmp_types.init ();
-         ignore (check ()))
-      ()
+  if Options.Check.get () then begin
+    Gmp_types.init ();
+    ignore (check ())
+  end
 
 let () = Db.Main.extend main
 

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

@@ -63,13 +63,6 @@ module Valid =
       let help = "translate annotation which have been proven valid"
     end)
 
-module Prepare =
-  False
-    (struct
-      let option_name = "-e-acsl-prepare"
-      let help = "prepare the AST to be directly usable by E-ACSL"
-    end)
-
 module Gmp_only =
   False
     (struct
@@ -174,6 +167,6 @@ let dkey_typing = register_category "typing"
 
 (*
 Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../.."
 End:
 *)

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

@@ -25,7 +25,6 @@ include Plugin.S (** implementation of Log.S for E-ACSL *)
 module Check: Parameter_sig.Bool
 module Run: Parameter_sig.Bool
 module Valid: Parameter_sig.Bool
-module Prepare: Parameter_sig.Bool
 module Gmp_only: Parameter_sig.Bool
 module Full_mmodel: Parameter_sig.Bool
 module Project_name: Parameter_sig.String
@@ -49,6 +48,6 @@ val dkey_typing: category
 
 (*
 Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../.."
 End:
 *)

src/plugins/e-acsl/src/project_initializer/keep_status.ml

@@ -49,7 +49,7 @@ type kind =
   | K_Requires
   | K_Ensures
 
-let pretty_kind fmt k =
+let _pretty_kind fmt k =
   Format.fprintf fmt "%s"
     (match k with
      | K_Assert -> "assert"
@@ -119,11 +119,11 @@ let before_translation () =
   (* reset all counters *)
   Datatype.String.Hashtbl.iter (fun _ info -> info.cpt <- 0) keep_status
 
-let must_translate kf kind =
+let must_translate _kf _kind = true
   (*  Options.feedback "GETTING %a for %a"
       pretty_kind kind
       Kernel_function.pretty kf;*)
-  !option_check
+(*  !option_check
   ||
   !option_valid
   ||
@@ -154,7 +154,7 @@ let must_translate kf kind =
         Kernel_function.pretty kf;
     keep
   with Not_found -> true
-
+*)
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."