From 821d828e56d1b3e74a1a5cdfaebe71866517f96f Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 20 Sep 2021 16:08:34 +0200
Subject: [PATCH] [eacsl] Move the check and initialization of options in a
dedicated function
---
src/plugins/e-acsl/src/main.ml | 14 +--------
src/plugins/e-acsl/src/options.ml | 29 +++++++++++++++++++
src/plugins/e-acsl/src/options.mli | 5 ++++
.../e-acsl/src/project_initializer/rtl.ml | 6 +---
4 files changed, 36 insertions(+), 18 deletions(-)
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index 194e1e54f8e..179208761e5 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -40,19 +40,7 @@ let generate_code =
(fun name ->
Options.feedback "beginning translation.";
Temporal.enable (Options.Temporal_validity.get ());
- if Plugin.is_present "variadic" then begin
- let opt_name = "-variadic-translation" in
- if Dynamic.Parameter.Bool.get opt_name () &&
- Options.Validate_format_strings.get () then begin
- if Ast.is_computed () then
- Options.abort
- "The variadic translation is incompatible with E-ACSL option \
- '%s'.@ Please use option '-variadic-no-translation'."
- Options.Validate_format_strings.option_name;
- Options.warning "deactivating variadic translation";
- Dynamic.Parameter.Bool.off opt_name ();
- end
- end;
+ Options.setup ();
(* slightly more efficient to copy the project before computing the AST
if it is not yet computed *)
let rtl_prj_name = Options.Project_name.get () ^ " RTL" in
diff --git a/src/plugins/e-acsl/src/options.ml b/src/plugins/e-acsl/src/options.ml
index e4f6bdddd94..cc172a073cc 100644
--- a/src/plugins/e-acsl/src/options.ml
+++ b/src/plugins/e-acsl/src/options.ml
@@ -177,6 +177,35 @@ let dkey_prepare = register_category "preparation"
let dkey_translation = register_category "translation"
let dkey_typing = register_category "typing"
+let setup ?(rtl=false) () =
+ (* Variadic translation *)
+ if Plugin.is_present "variadic" then begin
+ let opt_name = "-variadic-translation" in
+ if Dynamic.Parameter.Bool.get opt_name () then begin
+ if rtl then
+ (* If we are translating the RTL project, then we need to deactivate the
+ variadic translation. Indeed since we are translating the RTL in
+ isolation, we do not now if the variadic functions are used by the
+ user project and we cannot monomorphise them accordingly. *)
+ Dynamic.Parameter.Bool.off opt_name ()
+ else if Validate_format_strings.get () then begin
+ if Ast.is_computed () then
+ abort
+ "The variadic translation is incompatible with E-ACSL option \
+ '%s'.@ Please use option '-variadic-no-translation'."
+ Validate_format_strings.option_name;
+ warning ~once:true "deactivating variadic translation";
+ Dynamic.Parameter.Bool.off opt_name ();
+ end
+ end
+ end;
+ (* Additionnal kernel options while parsing the RTL project. *)
+ if rtl then begin
+ Kernel.Keep_unused_specified_functions.off ();
+ Kernel.CppExtraArgs.add
+ (Format.asprintf " -DE_ACSL_MACHDEP=%s" (Kernel.Machdep.get ()));
+ end
+
(*
Local Variables:
compile-command: "make -C ../../../.."
diff --git a/src/plugins/e-acsl/src/options.mli b/src/plugins/e-acsl/src/options.mli
index eda2b4a31e1..ec3f385c089 100644
--- a/src/plugins/e-acsl/src/options.mli
+++ b/src/plugins/e-acsl/src/options.mli
@@ -46,6 +46,11 @@ val dkey_prepare: category
val dkey_translation: category
val dkey_typing: category
+val setup: ?rtl:bool -> unit -> unit
+(** Verify and initialize the options of the current project according to the
+ options set by the user.
+ If [rtl] is true, then the project being modified is the RTL project. *)
+
(*
Local Variables:
compile-command: "make -C ../../../.."
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml
index 2666f703499..c48aa7a7e8f 100644
--- a/src/plugins/e-acsl/src/project_initializer/rtl.ml
+++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml
@@ -31,11 +31,7 @@ let create_rtl_ast prj =
prj
(fun () ->
(* compute the RTL AST in the standard E-ACSL setting *)
- if Plugin.is_present "variadic" then
- Dynamic.Parameter.Bool.off "-variadic-translation" ();
- Kernel.Keep_unused_specified_functions.off ();
- Kernel.CppExtraArgs.add
- (Format.asprintf " -DE_ACSL_MACHDEP=%s" (Kernel.Machdep.get ()));
+ Options.setup ~rtl:true ();
Kernel.Files.set [ rtl_file () ];
Ast.get ())
()
--
GitLab