diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index 0c6c931c4754a04db314b86e69710985c304155f..36ade122dc3459e0d29761256335671b85e3b411 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/options.ml b/src/plugins/e-acsl/src/options.ml
index deadac84c8111f20817897f5e2178155af4d9bf4..0723d4300b24f00392046a26748031d30690059a 100644
--- a/src/plugins/e-acsl/src/options.ml
+++ b/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:
*)
diff --git a/src/plugins/e-acsl/src/options.mli b/src/plugins/e-acsl/src/options.mli
index a3fc3697cbb0c0b072dfafc338c8ee02ddb9d273..d42a088cb71655a3afe6aa1b2e824112d79cf25d 100644
--- a/src/plugins/e-acsl/src/options.mli
+++ b/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:
*)
diff --git a/src/plugins/e-acsl/src/project_initializer/keep_status.ml b/src/plugins/e-acsl/src/project_initializer/keep_status.ml
index f4b83a501b0900b1e0599e48031a3a0f033a82b9..93580c24d45643672906c9b4a7616977d5179420 100644
--- a/src/plugins/e-acsl/src/project_initializer/keep_status.ml
+++ b/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 ../../../../.."