From 79c8e91d8de017fe0de588f16bacc1121f3eec0e Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 7 Apr 2020 11:30:22 +0200
Subject: [PATCH] [e-acsl] remove option -e-acsl-check
---
src/plugins/e-acsl/src/main.ml | 4 ----
src/plugins/e-acsl/src/options.ml | 7 -------
src/plugins/e-acsl/src/options.mli | 1 -
src/plugins/e-acsl/src/project_initializer/keep_status.ml | 3 +--
4 files changed, 1 insertion(+), 14 deletions(-)
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index 36ade122dc3..caa37aa4bce 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -172,10 +172,6 @@ let main () =
if Options.Run.get () then begin
change_printer ();
ignore (generate_code (Options.Project_name.get ()));
- end else
- 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 0723d4300b2..8c98ca16579 100644
--- a/src/plugins/e-acsl/src/options.ml
+++ b/src/plugins/e-acsl/src/options.ml
@@ -31,13 +31,6 @@ module P = Plugin.Register
module PP = P (* [PP] required to avoid an ocamldoc error in OCaml 4.02 *)
include PP
-module Check =
- False
- (struct
- let option_name = "-e-acsl-check"
- let help = "only type check E-ACSL annotated program"
- end)
-
module Run =
False
(struct
diff --git a/src/plugins/e-acsl/src/options.mli b/src/plugins/e-acsl/src/options.mli
index d42a088cb71..d5065c6a51d 100644
--- a/src/plugins/e-acsl/src/options.mli
+++ b/src/plugins/e-acsl/src/options.mli
@@ -22,7 +22,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 Gmp_only: Parameter_sig.Bool
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 93580c24d45..aa933b5f1a4 100644
--- a/src/plugins/e-acsl/src/project_initializer/keep_status.ml
+++ b/src/plugins/e-acsl/src/project_initializer/keep_status.ml
@@ -86,8 +86,7 @@ let option_check = ref false
let clear () =
Datatype.String.Hashtbl.clear keep_status;
- option_valid := Options.Valid.get ();
- option_check := Options.Check.get ()
+ option_valid := Options.Valid.get ()
let push kf kind ppt =
(* Options.feedback "PUSHING %a for %a"
--
GitLab