diff --git a/src/libraries/datatype/datatype.ml b/src/libraries/datatype/datatype.ml
index e130e39dd4b9c2988caa553d429038604ec6d54c..8dae3ee8845863d16cf056b3afe010dc63f141d0 100644
--- a/src/libraries/datatype/datatype.ml
+++ b/src/libraries/datatype/datatype.ml
@@ -265,6 +265,17 @@ module type Hashtbl = sig
module Make(Data: S) : S with type t = Data.t t
end
+module type S_with_set_and_map = sig
+ include S
+ module Set: Set with type elt = t
+ module Map: Map with type key = t
+end
+
+module type S_with_hashtbl = sig
+ include S
+ module Hashtbl: Hashtbl with type key = t
+end
+
module type S_with_collections = sig
include S
module Set: Set with type elt = t
@@ -1459,7 +1470,7 @@ end
(** {2 Simple type values} *)
(* ****************************************************************************)
-module With_collections(X: S)(Info: Functor_info) = struct
+module With_set_and_map(X: S)(Info: Functor_info) = struct
module D = X
include D
@@ -1476,6 +1487,18 @@ module With_collections(X: S)(Info: Functor_info) = struct
(D)
(struct let module_name = Info.module_name ^ ".Map" end)
+end
+
+module Make_with_set_and_map(X: Make_input) =
+ With_set_and_map
+ (Make(X))
+ (struct let module_name = String.capitalize_ascii X.name end)
+
+module With_hashtbl(X: S)(Info: Functor_info) = struct
+
+ module D = X
+ include D
+
module Hashtbl =
Hashtbl
(struct
@@ -1503,6 +1526,16 @@ module With_collections(X: S)(Info: Functor_info) = struct
end
+module Make_with_hashtbl(X: Make_input) =
+ With_hashtbl
+ (Make(X))
+ (struct let module_name = String.capitalize_ascii X.name end)
+
+module With_collections(X: S)(Info: Functor_info) = struct
+ include (With_set_and_map(X)(Info) : S_with_set_and_map with type t = X.t)
+ include (With_hashtbl(X)(Info) : S_with_hashtbl with type t := X.t)
+end
+
module Make_with_collections(X: Make_input) =
With_collections
(Make(X))
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index c063b0fa6d5f16c814946597fd18e63331e108c5..afef4bed64d218fccfd665079b7a18b5e256173b 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -267,6 +267,28 @@ module type Hashtbl = sig
end
+(** A datatype for a type [t] extended with predefined hashtbl over [t].
+ @since Frama-C+dev
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
+*)
+module type S_with_hashtbl = sig
+ include S
+ module Hashtbl: Hashtbl with type key = t
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
+end
+
+(** A datatype for a type [t] extended with predefined set and map over [t].
+ @since Frama-C+dev
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
+*)
+module type S_with_set_and_map = sig
+ include S
+ module Set: Set with type elt = t
+ (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
+
+ module Map: Map with type key = t
+end
+
(** A datatype for a type [t] extended with predefined set, map and hashtbl
over [t].
@@ -282,6 +304,30 @@ module type S_with_collections = sig
(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
end
+(** Generic comparable datatype builder: functions [equal] and [compare] must
+ not be {!undefined}.
+ @since Frama-C+dev *)
+module Make_with_set_and_map(X: Make_input):
+ S_with_set_and_map with type t = X.t
+
+(** Add sets and maps to an existing datatype, provided the [equal] and
+ [compare] are not {!undefined}.
+ @since Frama-C+dev *)
+module With_set_and_map(X: S)(_: Functor_info):
+ S_with_set_and_map with type t = X.t
+
+(** Generic comparable datatype builder: functions [equal] and [hash] must not
+ be {!undefined}.
+ @since Frama-C+dev *)
+module Make_with_hashtbl(X: Make_input):
+ S_with_hashtbl with type t = X.t
+
+(** Add hashtables modules to an existing datatype, provided the [equal] and
+ [hash] functions are not {!undefined}.
+ @since Frama-C+dev *)
+module With_hashtbl(X: S)(_: Functor_info):
+ S_with_hashtbl with type t = X.t
+
(** Generic comparable datatype builder: functions [equal], [compare] and
[hash] must not be {!undefined}. *)
module Make_with_collections(X: Make_input):
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index c9f3d079fecaa70e989acc52f319d5f89a27e3a1..e5a247efe9bec1d781e213268217339d91ded0f5 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -138,7 +138,7 @@ end = struct
= Id_term_in_profile.Hashtbl.create 97
(* Small functor to access the result of a memoized inference *)
- module Accesses (X : Datatype.S_with_collections)
+ module Accesses (X : Datatype.S_with_hashtbl)
(Tbl: sig val tbl : ival Error.result X.Hashtbl.t end)
: sig
val get : X.Hashtbl.key -> ival Error.result
diff --git a/src/plugins/e-acsl/src/libraries/analyses_datatype.ml b/src/plugins/e-acsl/src/libraries/analyses_datatype.ml
index 831323f60a495b5c658df723add1b195f1841e1a..a224e8849ee66a099fc7c1b69fd3963cdfd44585 100644
--- a/src/plugins/e-acsl/src/libraries/analyses_datatype.ml
+++ b/src/plugins/e-acsl/src/libraries/analyses_datatype.ml
@@ -361,9 +361,10 @@ struct
end
module Id_term_in_profile =
- Datatype.Pair_with_collections
- (Misc.Id_term)
- (Profile)
+ Datatype.With_hashtbl
+ (Datatype.Pair
+ (Misc.Id_term)
+ (Profile))
(struct let module_name = "E_ACSL.Analyse.Id_term_in_profile" end)
(* Environment to handle recursive functions: this environment stores the logic
diff --git a/src/plugins/e-acsl/src/libraries/analyses_datatype.mli b/src/plugins/e-acsl/src/libraries/analyses_datatype.mli
index 7981716f80c028963040f16003a03f754f1c937d..fcfc175386bb77c3de89ae5a5f80b1bf1d9fb3ff 100644
--- a/src/plugins/e-acsl/src/libraries/analyses_datatype.mli
+++ b/src/plugins/e-acsl/src/libraries/analyses_datatype.mli
@@ -68,7 +68,7 @@ end
(** term with a profile: a term inside a logic function or predicate may
contain free variables. The profile indicates the interval for those
free variables. *)
-module Id_term_in_profile: Datatype.S_with_collections
+module Id_term_in_profile: Datatype.S_with_hashtbl
with type t = term * Profile.t
(** profile of logic function or predicate: a logic info representing a logic
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 3c8849e72a984b1cd24744c43f618caf99c77208..3ca15998165cd90db2cee600fb7f4b713a5b6549 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -213,13 +213,11 @@ let name_of_binop = function
| MinusPP | MinusPI | PlusPI -> assert false
module Id_term =
- Datatype.Make_with_collections
+ Datatype.Make_with_hashtbl
(struct
include Cil_datatype.Term
let name = "E_ACSL.Id_term"
- let compare _ _ =
- (* There is no sound comparison based on physical identity. *)
- Kernel.fatal "Id_term: comparison undefined (and undefinable)"
+ let compare = Datatype.undefined
let equal (t1:term) t2 = t1 == t2
let structural_descr = Structural_descr.t_abstract
let rehash = Datatype.identity
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index 82f6b580aa35f9f00d62909a975aa184fd4c136f..f53ee5b4ae8d18d3574b6f94b37faaeaa8e1e618 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -81,7 +81,7 @@ val name_of_binop: binop -> string
val finite_min_and_max: Ival.t -> Integer.t * Integer.t
(** [finite_min_and_max i] takes the finite ival [i] and returns its bounds. *)
-module Id_term: Datatype.S_with_collections with type t = term
+module Id_term: Datatype.S_with_hashtbl with type t = term
(** Datatype for terms that relies on physical equality.
Note that of its collections only [Hashtbl] can be used.
Using [Map] and [Set] raises a fatal error as they require a comparison