From ebdcacd3ec889fbee111947e006fb6a0300255e2 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thibault.martin@cea.fr>
Date: Wed, 27 Mar 2019 17:16:23 +0100
Subject: [PATCH] Remove option -wp-assert-check-only
Since commit #8783731f and #28139960 this option is not needed anymore.
I updated LUncov (which was the only plugin using it) to remove it as well
---
src/plugins/wp/wpAnnot.ml | 2 +-
src/plugins/wp/wp_parameters.ml | 11 -----------
src/plugins/wp/wp_parameters.mli | 1 -
3 files changed, 1 insertion(+), 13 deletions(-)
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index b0203265ab2..1e2ce76c94b 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -914,7 +914,7 @@ let get_stmt_annots config v s =
in (b_acc, (a_acc, e_acc))
| TBRok | TBRpart ->
let id = WpPropId.mk_assert_id config.kf s a in
- let check = kind = Check || Wp_parameters.Assert_check_only.get ()
+ let check = kind = Check
and goal = goal_to_select config id in
if check && not goal then acc
else
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index bd5be9fa57d..3ea59dcff6c 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -897,17 +897,6 @@ module Check =
end)
let () = on_reset Print.clear
-let () = Parameter_customize.set_group wp_po
-let () = Parameter_customize.do_not_save ()
-let () = Parameter_customize.is_invisible ()
-module Assert_check_only =
- False (struct
- let option_name = "-wp-assert-check-only"
- let help =
- "Turns assertions into labels."
- end)
-let () = on_reset Print.clear
-
(* -------------------------------------------------------------------------- *)
(* --- OS environment variables --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 724fc39ae51..88dfd0553b3 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -135,7 +135,6 @@ module ReportJson: Parameter_sig.String
module ReportName: Parameter_sig.String
module MemoryContext: Parameter_sig.Bool
module Check: Parameter_sig.Bool
-module Assert_check_only: Parameter_sig.Bool
(** {2 Environment Variables} *)
--
GitLab