From 7bf0541061ead925333ccb17d491112657c9b639 Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Fri, 20 Sep 2024 19:45:36 +0200
Subject: [PATCH] [e-acsl] undefine comparison function for Id_term
The notion of equality of Id_term is physical equality. The comparison
as defined is not correct. If two terms are not physically equal but
structually equal the comparison returns 0. There is no meaningful way
to define a comparison w.r.t physical equality semantics, so we'll raise
an exception.
Not having any comparison implies that Map and Set cannot be used on
Id_term.t. Hashtbl is the only collection that still works. In the
subsequent commits the uses of Id_term.Map end Set will be changed to use
Id_term.Hashtbl instead.
Note that Datatype.undefined cannot be used here. In its current state
Datatypes.Make_with_collections requires comparison to be defined. In
the future we might tease out of Make_with_collections a functor
Make_with_hashtbl.
---
src/plugins/e-acsl/src/libraries/misc.ml | 5 +++--
src/plugins/e-acsl/src/libraries/misc.mli | 5 ++++-
2 files changed, 7 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 839b26676fd..e1ea93a8e4b 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -217,8 +217,9 @@ module Id_term =
(struct
include Cil_datatype.Term
let name = "E_ACSL.Id_term"
- let compare (t1:term) t2 =
- if t1 == t2 then 0 else Cil_datatype.Term.compare t1 t2
+ let compare _ _ =
+ (* There is no sound comparison based on physical identity. *)
+ Kernel.fatal "Id_term: comparison undefined (and undefinable)"
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 16706184a7f..b1bff7698f6 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -82,7 +82,10 @@ 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
-(** Datatype for terms that relies on physical equality. *)
+(** 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
+ function, which cannot be defined in a sound way for physical equality. *)
val extract_uncoerced_lval: exp -> exp option
(** Unroll the [CastE] part of the expression until an [Lval] is found, and
--
GitLab