From 5af97862d6a0f7518714804b3c1c763e60ef7b25 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 28 Jan 2025 15:57:53 +0100
Subject: [PATCH] [e-acsl] use Datatype.undefined for Misc.Id_term.compare
---
src/plugins/e-acsl/src/analyses/interval.ml | 2 +-
src/plugins/e-acsl/src/libraries/analyses_datatype.ml | 7 ++++---
src/plugins/e-acsl/src/libraries/analyses_datatype.mli | 2 +-
src/plugins/e-acsl/src/libraries/misc.ml | 6 ++----
src/plugins/e-acsl/src/libraries/misc.mli | 2 +-
5 files changed, 9 insertions(+), 10 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index c9f3d079fec..e5a247efe9b 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 831323f60a4..a224e8849ee 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 7981716f80c..fcfc175386b 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 3c8849e72a9..3ca15998165 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 82f6b580aa3..f53ee5b4ae8 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
--
GitLab