Skip to content
Snippets Groups Projects
Commit 69ca6dff authored by Cécile Ruet-Cros's avatar Cécile Ruet-Cros Committed by Loïc Correnson
Browse files

[wp] remove stuff

parent fb7ababa
No related branches found
No related tags found
No related merge requests found
...@@ -216,15 +216,6 @@ struct ...@@ -216,15 +216,6 @@ struct
end 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 --- *) (* --- Data Layout --- *)
......
...@@ -261,25 +261,4 @@ end ...@@ -261,25 +261,4 @@ end
(** {2 Options} *) (** {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
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
...@@ -284,95 +284,6 @@ module Volatile = ...@@ -284,95 +284,6 @@ module Volatile =
Use -wp-no-volatile to ignore volatile attributes." Use -wp-no-volatile to ignore volatile attributes."
end) 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 --- *) (* --- WP Strategy --- *)
(* ------------------------------------------------------------------------ *) (* ------------------------------------------------------------------------ *)
......
...@@ -64,16 +64,6 @@ module Literals : Parameter_sig.Bool ...@@ -64,16 +64,6 @@ module Literals : Parameter_sig.Bool
module Volatile : Parameter_sig.Bool module Volatile : Parameter_sig.Bool
module WeakIntModel : 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} *) (** {2 Computation Strategies} *)
module Init: Parameter_sig.Bool module Init: Parameter_sig.Bool
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment