From 69ca6dff929b654c7ef7224273e93de74129dd19 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr>
Date: Thu, 22 Aug 2024 09:48:16 +0200
Subject: [PATCH] [wp] remove stuff
---
src/plugins/wp/Layout.ml | 9 ----
src/plugins/wp/Layout.mli | 21 --------
src/plugins/wp/wp_parameters.ml | 89 --------------------------------
src/plugins/wp/wp_parameters.mli | 10 ----
4 files changed, 129 deletions(-)
diff --git a/src/plugins/wp/Layout.ml b/src/plugins/wp/Layout.ml
index 39b59cd426a..6661a8ddf21 100644
--- a/src/plugins/wp/Layout.ml
+++ b/src/plugins/wp/Layout.ml
@@ -216,15 +216,6 @@ struct
end
-module Mode(OPT : sig val get : unit -> bool end) =
-struct
- let default = OPT.get
- let merge a b = if default () then a && b else a || b
-end
-
-module RW = Mode(Wp.Region_rw)
-module Flat = Mode(Wp.Region_flat)
-module Pack = Mode(Wp.Region_pack)
(* -------------------------------------------------------------------------- *)
(* --- Data Layout --- *)
diff --git a/src/plugins/wp/Layout.mli b/src/plugins/wp/Layout.mli
index 5370aa2299e..1db68dd9fa0 100644
--- a/src/plugins/wp/Layout.mli
+++ b/src/plugins/wp/Layout.mli
@@ -261,25 +261,4 @@ end
(** {2 Options} *)
(* -------------------------------------------------------------------------- *)
-(** Read-Write access *)
-module RW :
-sig
- val default : unit -> bool
- val merge : bool -> bool -> bool
-end
-
-(** Flatten arrays *)
-module Flat :
-sig
- val default : unit -> bool
- val merge : bool -> bool -> bool
-end
-
-(** Pack fields *)
-module Pack :
-sig
- val default : unit -> bool
- val merge : bool -> bool -> bool
-end
-
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index a0334d13b33..9268c9e87a8 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -284,95 +284,6 @@ module Volatile =
Use -wp-no-volatile to ignore volatile attributes."
end)
-(* -------------------------------------------------------------------------- *)
-(* --- Region Model --- *)
-(* -------------------------------------------------------------------------- *)
-
-let wp_region = add_group "Region Analysis"
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region =
- False
- (struct
- let option_name = "-wp-region"
- let help = "Perform Region Analysis (experimental)"
- end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_fixpoint =
- True
- (struct
- let option_name = "-wp-region-fixpoint"
- let help = "Compute region aliasing fixpoint"
- end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_cluster =
- True
- (struct
- let option_name = "-wp-region-cluster"
- let help = "Compute region clustering fixpoint"
- end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_inline =
- True
- (struct
- let option_name = "-wp-region-inline"
- let help = "Inline aliased sub-clusters"
- end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_rw =
- True
- (struct
- let option_name = "-wp-region-rw"
- let help = "Written region are considered read-write by default"
- end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_pack =
- True
- (struct
- let option_name = "-wp-region-pack"
- let help = "Pack clusters by default"
- end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_flat =
- False
- (struct
- let option_name = "-wp-region-flat"
- let help = "Flatten arrays by default"
- end)
-
-let () = Parameter_customize.set_group wp_region
-module Region_annot =
- False
- (struct
- let option_name = "-region-annot"
- let help = "Register '@region' ACSL Annotations (auto with -wp-region)"
- end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.is_invisible ()
-module Region_output_dot =
- Filepath
- (struct
- let option_name = "-wp-region-output-dot"
- let arg_name = "output.dot"
- let file_kind = "DOT"
- let existence = Fc_Filepath.Indifferent
- let help = "Outputs the region graph in DOT format to the specified file."
- end)
-
(* ------------------------------------------------------------------------ *)
(* --- WP Strategy --- *)
(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 5c5159c59b5..84a25a418c3 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -64,16 +64,6 @@ module Literals : Parameter_sig.Bool
module Volatile : Parameter_sig.Bool
module WeakIntModel : Parameter_sig.Bool
-module Region: Parameter_sig.Bool
-module Region_rw: Parameter_sig.Bool
-module Region_pack: Parameter_sig.Bool
-module Region_flat: Parameter_sig.Bool
-module Region_annot: Parameter_sig.Bool
-module Region_inline: Parameter_sig.Bool
-module Region_fixpoint: Parameter_sig.Bool
-module Region_cluster: Parameter_sig.Bool
-module Region_output_dot : Parameter_sig.Filepath
-
(** {2 Computation Strategies} *)
module Init: Parameter_sig.Bool
--
GitLab