From 52d39bfe6d149ff923c2ec985da39cdeff51c94f Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 11 Oct 2019 12:16:07 +0200
Subject: [PATCH] [archi] restore some Frama-C invariants for the generated
code
---
src/plugins/e-acsl/src/code_generator/env.ml | 4 +++-
.../e-acsl/src/code_generator/injector.ml | 16 +++++++++++-----
src/plugins/e-acsl/src/code_generator/loops.ml | 3 +--
src/plugins/e-acsl/src/code_generator/loops.mli | 2 +-
src/plugins/e-acsl/src/main.ml | 2 --
5 files changed, 16 insertions(+), 11 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 9c0be44c094..02b4b7faa95 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/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 ])
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 43ea6d2192f..10ff14fd0dd 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/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:
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index eb4b4dd7493..d8b4ff6664e 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/code_generator/loops.mli b/src/plugins/e-acsl/src/code_generator/loops.mli
index a37b5beaee7..a93afb4cb6b 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.mli
+++ b/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.
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index 4b0ccaabdf1..04623b1a012 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/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). *)
--
GitLab