[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

@@ -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

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