diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 0a87aa8f1fd6414128dea862b440a281fe158ffd..87b585b9c4894500291e4c53141699f9a1b0de7d 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -452,7 +452,6 @@ module Base = struct
let copy = Datatype.undefined
end)
let id = id
- let pretty_debug = pretty
end
include Base
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 7d64c801fb99d13edc99597d07ac6b5c3860a20b..9bc8df0beb23556775b5f700474bfa6375472d1a 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -1024,7 +1024,6 @@ let bitwise_not ~size ~signed v =
else
bitwise_unsigned_not ~size v
-let pretty_debug = pretty
let name = "ival"
(*
diff --git a/src/kernel_services/abstract_interp/ival.mli b/src/kernel_services/abstract_interp/ival.mli
index aadd4ff07595952ff9b725b57a7df3022fca96f6..0ef0bbfb577724b2c547afa72fe24a017f453fb8 100644
--- a/src/kernel_services/abstract_interp/ival.mli
+++ b/src/kernel_services/abstract_interp/ival.mli
@@ -330,8 +330,6 @@ val complement_int_under: size:int -> signed:bool -> t -> t Lattice_bounds.or_bo
(** Returns an under-approximation of the integers of the given size and
signedness that are *not* represented by the given ival. *)
-val pretty_debug : Format.formatter -> t -> unit
-
(**/**)
val rehash: t -> t (* Low-level operation for demarshalling *)
diff --git a/src/kernel_services/analysis/stmts_graph.ml b/src/kernel_services/analysis/stmts_graph.ml
index f93858ebf92a9591bffed2eec02c60bc21758148..342f5ba62ce6c0510812edd702e1ae7f790a83b7 100644
--- a/src/kernel_services/analysis/stmts_graph.ml
+++ b/src/kernel_services/analysis/stmts_graph.ml
@@ -34,7 +34,7 @@ struct
module HV = Hashtbl.Make(Stmt)
module HptmapStmtBool = Hptmap.Make
(Cil_datatype.Stmt_Id)
- (struct include Datatype.Bool let pretty_debug = pretty end)
+ (Datatype.Bool)
(struct
let initial_values = []
let dependencies = [ Ast.self ]
diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml
index a4678edd33bc1724d842ef5d1628a987a491fa39..7766433682c661555a31392920d1d112d28675f3 100644
--- a/src/libraries/utils/hptmap.ml
+++ b/src/libraries/utils/hptmap.ml
@@ -130,11 +130,6 @@ module type Id_Datatype = sig
val id: t -> int
end
-module type V = sig
- include Datatype.S
- val pretty_debug: t Pretty_utils.formatter
-end
-
module Shape(Key: Id_Datatype) = struct
type key = Key.t
type 'b map = (Key.t, 'b) tree
@@ -599,7 +594,7 @@ end
module Make_with_compositional_bool
(Key: Id_Datatype)
- (V : V)
+ (V : Datatype.S)
(Compositional_bool : Compositional_bool with type key := Key.t
and type v := V.t)
(Info: Info with type key := Key.t
@@ -621,7 +616,7 @@ struct
"L@[<v>@[(A %x, T %a)@]@ @[(AK %x)%a@]@ @[ -> (AV %x)@]@ @[%a@]@]"
(Extlib.address_of_value t) Tag_comp.pretty comp
(Extlib.address_of_value k) Key.pretty k
- (Extlib.address_of_value v) V.pretty_debug v
+ (Extlib.address_of_value v) V.pretty v
| Branch (prefix, mask, t1, t2, tag) as t ->
Format.fprintf fmt
"B@[<v>@[(A %x, T %a, P %x, M %x)@]@ @[%a@]@ @[ %a@]@]"
@@ -1437,8 +1432,11 @@ module Comp_unused = struct
let compose _ _ = false
end
-module Make (Key: Id_Datatype) (V : V) (Info: Info with type key := Key.t
- and type v := V.t)
+module Make
+ (Key: Id_Datatype)
+ (V : Datatype.S)
+ (Info: Info with type key := Key.t
+ and type v := V.t)
= Make_with_compositional_bool (Key) (V) (Comp_unused) (Info)
(*
diff --git a/src/libraries/utils/hptmap.mli b/src/libraries/utils/hptmap.mli
index 725c205712d55b769b762290d8f946501c61418f..cd2b5c0c3aeab48650f4b1eeb32aa264367bd090 100644
--- a/src/libraries/utils/hptmap.mli
+++ b/src/libraries/utils/hptmap.mli
@@ -39,12 +39,6 @@ module Shape (Key : Id_Datatype): sig
type 'a t = 'a map
end
-(** Values stored in the map *)
-module type V = sig
- include Datatype.S
- val pretty_debug: t Pretty_utils.formatter
-end
-
(** Required information for the correctness of the hptmaps. *)
module type Info = sig
type key
@@ -65,7 +59,7 @@ end
to values [V]. *)
module Make
(Key : Id_Datatype)
- (V : V)
+ (V : Datatype.S)
(_ : Info with type key := Key.t
and type v := V.t)
: Hptmap_sig.S with type key = Key.t
@@ -94,7 +88,7 @@ end
each tree. *)
module Make_with_compositional_bool
(Key : Id_Datatype)
- (V : V)
+ (V : Datatype.S)
(_ : Compositional_bool with type key := Key.t
and type v := V.t)
(_ : Info with type key := Key.t
diff --git a/src/libraries/utils/hptset.ml b/src/libraries/utils/hptset.ml
index 28c3164935d6c7eda1a9c5785a494f921fa187a7..11e88615617ba3def5a710c98d77c0a90573dea8 100644
--- a/src/libraries/utils/hptset.ml
+++ b/src/libraries/utils/hptset.ml
@@ -110,17 +110,12 @@ module Make
type elt = X.t
- module Unit = struct
- include Datatype.Unit
- let pretty_debug = pretty
- end
-
module Hptmap_Info = struct
let initial_values = List.map (List.map (fun k -> k, ())) Info.initial_values
let dependencies = Info.dependencies
end
- module M = Hptmap.Make (X) (Unit) (Hptmap_Info)
+ module M = Hptmap.Make (X) (Datatype.Unit) (Hptmap_Info)
include M
let add k s = add k () s
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index aa4bb6a684b379d0379aec601585f5930e713cef..a317fca1878143ba241ca512e61dfed56eb30e47 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -188,7 +188,6 @@ module Deps: sig
include Datatype.S with type t := t
val pretty_precise: Format.formatter -> t -> unit
- val pretty_debug: Format.formatter -> t -> unit
(* Constructors *)
diff --git a/src/plugins/eva/domains/equality/equality.ml b/src/plugins/eva/domains/equality/equality.ml
index 7d85984fcb220a3f26a128b64e90edea10a08b20..ab2e0c45457c2433ea44f1c4c1e5acb33bafa686 100644
--- a/src/plugins/eva/domains/equality/equality.ml
+++ b/src/plugins/eva/domains/equality/equality.ml
@@ -75,7 +75,6 @@ module Set = struct
the value of [lv], and the second set gathers the expressions that
contains [&lv]. *)
include Datatype.Triple (Equality) (HCESet) (HCESet)
- let pretty_debug = pretty
let inter (left_eq, left_set, left_set') (right_eq, right_set, right_set') =
let equality = Equality.inter left_eq right_eq
diff --git a/src/plugins/eva/domains/gauges/gauges_domain.ml b/src/plugins/eva/domains/gauges/gauges_domain.ml
index a082f4050440a84edf95113b425e4138c9f16f0c..49416c570c0ba4ba049997416964df3af8801145 100644
--- a/src/plugins/eva/domains/gauges/gauges_domain.ml
+++ b/src/plugins/eva/domains/gauges/gauges_domain.ml
@@ -65,7 +65,6 @@ module G = struct
| Some i -> Abstract_interp.Int.pretty fmt i
in
Format.fprintf fmt "[%a .. %a]" (pp_bound '-') min (pp_bound '+') max
- let pretty_debug = pretty
let inject_range n1 n2 : t =
Some (Integer.of_int (min n1 n2)), Some (Integer.of_int (max n1 n2))
diff --git a/src/plugins/eva/domains/hcexprs.ml b/src/plugins/eva/domains/hcexprs.ml
index 951d897535f741e15798eada777b81ce6fc4566a..b0fd18a76ac936bf73ca1abf185414ced2510329 100644
--- a/src/plugins/eva/domains/hcexprs.ml
+++ b/src/plugins/eva/domains/hcexprs.ml
@@ -96,8 +96,6 @@ module HCE = struct
include S
- let pretty_debug = pretty
-
let of_lval lv = hashcons (LV lv)
let of_exp (exp : Eva_ast.exp) =
diff --git a/src/plugins/eva/domains/hcexprs.mli b/src/plugins/eva/domains/hcexprs.mli
index 0b65e6e224e4ef934e90f4bc6462398b6fecce50..72cc5f976e11f3f4e1c9b71330f8dab3179a4a8b 100644
--- a/src/plugins/eva/domains/hcexprs.mli
+++ b/src/plugins/eva/domains/hcexprs.mli
@@ -40,7 +40,6 @@ module E: Datatype.S with type t = unhashconsed_exprs
module HCE: sig
include Datatype.S_with_collections
val self: State.t
- val pretty_debug: t Pretty_utils.formatter
val id: t -> int
diff --git a/src/plugins/eva/domains/multidim/abstract_structure.ml b/src/plugins/eva/domains/multidim/abstract_structure.ml
index eac548f2d772761ae0e8193a24fddf4df61e8898..d8301b01b2178008fb669823eeb8bdd99c108526 100644
--- a/src/plugins/eva/domains/multidim/abstract_structure.ml
+++ b/src/plugins/eva/domains/multidim/abstract_structure.ml
@@ -75,7 +75,6 @@ struct
let name = "Abstract_Memory.Structure.Values"
let reprs = [ of_raw Bit.zero ]
end)
- let pretty_debug = pretty
end
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index 63db3c5dc729efcc005e03c1643ae3ebbe62ea60..ed430145d4c7c6edb1325d1bd53de2c18e100429 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -265,7 +265,6 @@ struct
include Datatype.Make (Prototype)
let pretty = Memory.pretty
- let _pretty_debug = Memory.pretty
let top = Memory.top
let is_top = Memory.is_top
let is_included = Memory.is_included
@@ -333,7 +332,6 @@ struct
module V =
struct
include Datatype.Pair (Memory) (Referers)
- let pretty_debug = pretty
let top = Memory.top, Referers.empty
let is_top (m,r) = Memory.is_top m && Referers.is_empty r
end
diff --git a/src/plugins/eva/domains/numerors/numerors_value.ml b/src/plugins/eva/domains/numerors/numerors_value.ml
index 85485626c68e224449714f1415886299c7dd3b84..ee85f4a742c570ba4865727090b3183485de150e 100644
--- a/src/plugins/eva/domains/numerors/numerors_value.ml
+++ b/src/plugins/eva/domains/numerors/numerors_value.ml
@@ -113,7 +113,6 @@ module T = struct
let pretty = pp_print
end
include Datatype.Make(T)
-let pretty_debug = pretty
let pretty_typ _ = pretty
type context = unit
diff --git a/src/plugins/eva/domains/numerors/numerors_value.mli b/src/plugins/eva/domains/numerors/numerors_value.mli
index 4814acb57a0edd21e9225483776dff5eb02dd811..721ef891ec3fab66b0db193cfd80477e1f7716e8 100644
--- a/src/plugins/eva/domains/numerors/numerors_value.mli
+++ b/src/plugins/eva/domains/numerors/numerors_value.mli
@@ -22,8 +22,6 @@
include Abstract_value.Leaf with type context = unit
-val pretty_debug : t Pretty_utils.formatter
-
(** Reduction of an error value according to a floating-point interval. *)
val reduce: Fval.t -> t -> t Eval.or_bottom
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index bd82bcbad8ae1825694919df741a606deb49fd84..e4a757b1b392dd667d16f78c6eb9e3c78e2c3aac 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -588,7 +588,6 @@ end
module Diamond = struct
include Datatype.Make (DiamondDatatype)
- let pretty_debug = pretty
let top = { add = Ival.top; sub = Ival.top }
@@ -736,9 +735,7 @@ end
(* Keep track of related variables in an octagon state. *)
module Relations = struct
- include Hptmap.Make (Variable)
- (struct include VarSet let pretty_debug = pretty end)
- (Hptmap_Info)
+ include Hptmap.Make (Variable) (VarSet) (Hptmap_Info)
let inter =
let cache = Hptmap_sig.PersistentCache "Octagons.Relations.inter" in
@@ -895,7 +892,6 @@ module BaseToVariables = struct
include Datatype.Pair
(VSet) (* Directly dependent variables *)
(VSet) (* Indirectly dependent variables *)
- let pretty_debug = pretty
let inter (s1,t1) (s2,t2) = VSet.inter s1 s2, VSet.inter t1 t2
let union (s1,t1) (s2,t2) = VSet.union s1 s2, VSet.union t1 t2
let is_empty (s, t) = VSet.is_empty s && VSet.is_empty t
diff --git a/src/plugins/eva/domains/simple_memory.ml b/src/plugins/eva/domains/simple_memory.ml
index e8a9140134e456b11f6c56614709d0538eaa7f53..b935f55c6a9ff5f85cf903041d57992a474808c0 100644
--- a/src/plugins/eva/domains/simple_memory.ml
+++ b/src/plugins/eva/domains/simple_memory.ml
@@ -28,7 +28,6 @@ module type Value = sig
include Abstract_value.Leaf
val widen : t -> t -> t
val track_variable: Cil_types.varinfo -> bool
- val pretty_debug: t Pretty_utils.formatter
val builtins: (string * t builtin) list
end
diff --git a/src/plugins/eva/domains/simple_memory.mli b/src/plugins/eva/domains/simple_memory.mli
index f70f75d573bc1628bd6a28ef413d2f5191c4c6c1..ae1cbfd0f875361a3c002a5f36ce44b019806710 100644
--- a/src/plugins/eva/domains/simple_memory.mli
+++ b/src/plugins/eva/domains/simple_memory.mli
@@ -40,9 +40,6 @@ module type Value = sig
mapped to [V.top]. *)
val track_variable: Cil_types.varinfo -> bool
- (** Can be equal to {!pretty} *)
- val pretty_debug: t Pretty_utils.formatter
-
(** A list of builtins for the domain: each builtin is associated with the
name of the C function it interprets. *)
val builtins: (string * t builtin) list
diff --git a/src/plugins/eva/domains/traces_domain.ml b/src/plugins/eva/domains/traces_domain.ml
index e45a1cbba8aebec2341d3289000b9a025b8841c5..5ca13666ef8b18020410e74dbc64eaaa80d66464 100644
--- a/src/plugins/eva/domains/traces_domain.ml
+++ b/src/plugins/eva/domains/traces_domain.ml
@@ -223,7 +223,6 @@ module EdgeList = struct
include Datatype.List_with_collections(Edge)
(struct let module_name = "Value.Traces_domain.EdgeList" end)
let pretty = Edge.pretty_list
- let pretty_debug = pretty
end
module Graph = struct
diff --git a/src/plugins/eva/types/callstack.ml b/src/plugins/eva/types/callstack.ml
index fec3d18684256394e847727bf854d578c0f3e644..922edd69df4382b6ea06aa2a9db64165964fbd4c 100644
--- a/src/plugins/eva/types/callstack.ml
+++ b/src/plugins/eva/types/callstack.ml
@@ -78,8 +78,6 @@ type call = Call.t
include Datatype.Make_with_collections (Prototype)
-let pretty_debug = pretty
-
let compare_lex cs1 cs2 =
if cs1 == cs2 then 0 else
let c = Thread.compare cs1.thread cs2.thread in
diff --git a/src/plugins/eva/types/callstack.mli b/src/plugins/eva/types/callstack.mli
index 0340490e58ec65c80c72e53357be16657c40c4aa..494df93cf7076aed3e79eb676f746d68c5036d7a 100644
--- a/src/plugins/eva/types/callstack.mli
+++ b/src/plugins/eva/types/callstack.mli
@@ -85,5 +85,3 @@ val to_stmt_list : t -> Cil_types.stmt list
val to_call_list : t -> (Cil_types.kernel_function * Cil_types.kinstr) list
[@@@ api_end]
-
-val pretty_debug : Format.formatter -> t -> unit
diff --git a/src/plugins/eva/types/deps.ml b/src/plugins/eva/types/deps.ml
index 9ac287585199f8a752f7c210da8d399e0f9872a5..31a37bf66a68c9645b955a3b9a5525a40ea1d62d 100644
--- a/src/plugins/eva/types/deps.ml
+++ b/src/plugins/eva/types/deps.ml
@@ -45,8 +45,6 @@ let pretty_precise fmt {data; indirect} =
Zone.pretty indirect
Zone.pretty data
-let pretty_debug = pretty_precise
-
(* Conversion to zone, used by default pretty printing *)
let to_zone d = Locations.Zone.join d.data d.indirect
diff --git a/src/plugins/eva/types/deps.mli b/src/plugins/eva/types/deps.mli
index 4dbd0ea993573958ea96cd8277a2472b4b82f3c9..9edd34e5ba2bc862a58c416f3a2fb660dae58bad 100644
--- a/src/plugins/eva/types/deps.mli
+++ b/src/plugins/eva/types/deps.mli
@@ -33,7 +33,6 @@ type t = {
include Datatype.S with type t := t
val pretty_precise: Format.formatter -> t -> unit
-val pretty_debug: Format.formatter -> t -> unit
(* Constructors *)
diff --git a/src/plugins/eva/values/sign_value.ml b/src/plugins/eva/values/sign_value.ml
index 04ab54aa224b3beb5389335ef7e2f9c60fd404f2..4e779b62672a27208d26949a468f999b7581e0e2 100644
--- a/src/plugins/eva/values/sign_value.ml
+++ b/src/plugins/eva/values/sign_value.ml
@@ -65,7 +65,6 @@ include Datatype.Make(struct
(if v.zero then "0" else "")
(if v.pos then "+" else "")
end)
-let pretty_debug = pretty
let pretty_typ _ = pretty
type context = unit
diff --git a/src/plugins/eva/values/sign_value.mli b/src/plugins/eva/values/sign_value.mli
index 7fadfe569703267e5dede1c083937d92099ea031..b1419e132b27a5a6f566d5d3e90368eea82a154a 100644
--- a/src/plugins/eva/values/sign_value.mli
+++ b/src/plugins/eva/values/sign_value.mli
@@ -29,4 +29,3 @@ type signs = {
}
include Abstract_value.Leaf with type t = signs and type context = unit
-val pretty_debug: t Pretty_utils.formatter
diff --git a/src/plugins/pdg/pdg_types/pdgTypes.ml b/src/plugins/pdg/pdg_types/pdgTypes.ml
index e4af154aef0ff40d9738a574f86e74de7f9946fc..7a8215b18c4388fb84bbc7c2fe2e63b6a66f16a7 100644
--- a/src/plugins/pdg/pdg_types/pdgTypes.ml
+++ b/src/plugins/pdg/pdg_types/pdgTypes.ml
@@ -224,14 +224,11 @@ module DpdZone : sig
val dpd_zone : t -> Locations.Zone.t option
val pretty : Format.formatter -> t -> unit
- val pretty_debug: Format.formatter -> t -> unit
end = struct
include Datatype.Pair(Dpd)(Datatype.Option(Locations.Zone))
(* None == Locations.Zone.Top *)
- let pretty_debug = pretty
-
let dpd_kind dpd = fst dpd
let dpd_zone dpd = snd dpd
let kind_and_zone dpd = dpd