[archi] restore some Frama-C invariants for the generated code

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

@@ -434,7 +434,9 @@ let pop_and_get ?(split=false) env stmt ~global_clear where =
        the final block does not contain any local, so may be transient. *)
     if split then
       match stmt.skind with
-      | Instr (Skip _) -> b
+      (* [TODO ARCHI] would result in nicer generated pieces of code, but
+       * killing statements has huge consequences on Frama-C invariants... *)
+      (*      | Instr (Skip _) -> b *)
       | _ ->
         let sblock = Cil.mkStmt ~valid_sid:true (Block b) in
         Cil.transient_block (Cil.mkBlock [ sblock; stmt ])

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

@@ -348,6 +348,7 @@ let add_new_block_in_stmt env kf stmt =
     "@[new stmt (from sid %d):@ %a@]" stmt.sid Printer.pp_stmt new_stmt;
   new_stmt, env
 
+(* [TODO ARCHI] not sure returning the stmt_kind is useful *)
 (* visit the substmts and build the new skind *)
 let rec inject_in_substmt env kf stmt = match stmt.skind with
   | Instr instr ->
@@ -748,23 +749,28 @@ let inject_in_file file =
   file.globals <- Logic_functions.add_generated_functions file.globals;
   inject_mmodel_initializer main
 
-let reset_all () =
+let reset_all ast =
+  Options.Run.off ();
   Misc.reset ();
   Logic_functions.reset ();
   Literal_strings.reset ();
   Global_observer.reset ();
-  Keep_status.before_translation ()
+  Typing.clear ();
+  Cfg.clearFileCFG ~clear_id:false ast;
+  Cfg.computeFileCFG ast;
+  Kernel_function.clear_sid_info ();
+  Ast.mark_as_grown ()
 
 let inject () =
   Options.feedback ~level:2
     "injecting annotations as code in project %a"
     Project.pretty (Project.current ());
-  reset_all ();
+  Keep_status.before_translation ();
   Misc.reorder_ast ();
   let ast = Ast.get () in
   inject_in_file ast;
-  (* [TODO ARCHI] not consistent with the [reset_all] strategy: *)
-  Typing.clear ()
+  Loops.apply_after_transformation ();
+  reset_all ast;
 
 (*
 Local Variables:

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

@@ -45,8 +45,7 @@ let term_to_exp_ref
 
 module Loop_invariants_actions = Hook.Make(struct end)
 
-let apply_after_transformation prj =
-  Project.on prj Loop_invariants_actions.apply ()
+let apply_after_transformation = Loop_invariants_actions.apply
 
 let mv_invariants kf ~old stmt =
   Options.feedback ~current:true ~level:3

src/plugins/e-acsl/src/code_generator/loops.mli

@@ -28,7 +28,7 @@ open Cil_types
 (************************* Loop invariants ********************************)
 (**************************************************************************)
 
-val apply_after_transformation: Project.t -> unit
+val apply_after_transformation: unit -> unit
 
 val mv_invariants: kernel_function -> old:stmt -> stmt -> unit
 (** Transfer the loop invariants from the [old] loop to the new one.

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

@@ -151,8 +151,6 @@ let generate_code =
                         Gmp_types.init ();
                         Mmodel_analysis.reset ();
                         Injector.inject ();
-                        (* [TODO ARCHI] remove the project as arguments *)
-                        Loops.apply_after_transformation copied_prj;
                         (* 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). *)