[e-acsl] remove option -e-acsl-check

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

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

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

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"