diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 539184f0204551c371fafc3292e6e754666cf95e..21f1075b8811610caaba1513e962b69ff2b4bca7 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -909,15 +909,26 @@ module Enumitem = struct
end)
end
-let compare_constant c1 c2 = match c1, c2 with
- | CInt64(v1,k1,_), CInt64(v2,k2,_) ->
- compare_chain Integer.compare v1 v2 Extlib.compare_basic k1 k2
+(* If [strict] is true, the comparaison of integer and floating-point constants
+ takes into account their textual representation (if any). Otherwise,
+ constants with the same type and value are equal even if their textual
+ representations differ. *)
+let compare_constant ~strict c1 c2 = match c1, c2 with
+ | CInt64(v1,k1,s1), CInt64(v2,k2,s2) ->
+ let r = compare_chain Integer.compare v1 v2 Extlib.compare_basic k1 k2 in
+ if r = 0 && strict
+ then Option.compare Datatype.String.compare s1 s2
+ else r
| CStr s1, CStr s2 -> Datatype.String.compare s1 s2
| CWStr s1, CWStr s2 -> compare_list Datatype.Int64.compare s1 s2
| CChr c1, CChr c2 -> Datatype.Char.compare c1 c2
- | CReal (f1,k1,_), CReal(f2,k2,_) ->
- compare_chain Datatype.Float.compare f1 f2
- Extlib.compare_basic k1 k2
+ | CReal (f1,k1,s1), CReal(f2,k2,s2) ->
+ let r =
+ compare_chain Datatype.Float.compare f1 f2 Extlib.compare_basic k1 k2
+ in
+ if r = 0 && strict
+ then Option.compare Datatype.String.compare s1 s2
+ else r
| CEnum e1, CEnum e2 -> Enumitem.compare e1 e2
| (CInt64 _, (CStr _ | CWStr _ | CChr _ | CReal _ | CEnum _)) -> 1
| (CStr _, (CWStr _ | CChr _ | CReal _ | CEnum _)) -> 1
@@ -934,16 +945,41 @@ let hash_const c =
| CInt64 (n,k,_) -> Integer.hash n + Hashtbl.hash k
| CEnum ei -> 95 + Enumitem.hash ei
+module type Make_cmp_input = sig
+ include Datatype.Make_input
+ val compare: strict:bool -> t -> t -> int
+end
+
+module Make_compare_non_strict(M: Make_cmp_input) =
+ Datatype.Make_with_collections(
+ struct
+ include M
+ let compare = M.compare ~strict:false
+ end)
+
+module Make_compare_strict(M: Make_cmp_input) =
+ Datatype.Make_with_collections(
+ struct
+ include M
+ let compare = M.compare ~strict:true
+ let name = M.name ^ "Strict"
+ end)
+
module StructEq =
struct
- let rec compare_exp e1 e2 =
+ (* If [strict] is true, the comparaison of integer and floating-point constants
+ takes into account their textual representation (if any). Otherwise,
+ constants with the same type and value are equal even if their textual
+ representations differ. *)
+ let rec compare_exp ~strict e1 e2 =
+ let compare_exp = compare_exp ~strict in
match e1.enode, e2.enode with
| Const (CStr _), Const (CStr _)
| Const (CWStr _), Const (CWStr _) -> compare e1.eid e2.eid
- | Const c1, Const c2 -> compare_constant c1 c2
+ | Const c1, Const c2 -> compare_constant ~strict c1 c2
| Const _, _ -> 1
| _, Const _ -> -1
- | Lval lv1, Lval lv2 -> compare_lval lv1 lv2
+ | Lval lv1, Lval lv2 -> compare_lval ~strict lv1 lv2
| Lval _, _ -> 1
| _, Lval _ -> -1
| SizeOf t1, SizeOf t2 -> Typ.compare t1 t2
@@ -985,40 +1021,40 @@ struct
if res = 0 then compare_exp e1 e2 else res
| CastE _, _ -> 1
| _, CastE _ -> -1
- | AddrOf lv1, AddrOf lv2 -> compare_lval lv1 lv2
+ | AddrOf lv1, AddrOf lv2 -> compare_lval ~strict lv1 lv2
| AddrOf _, _ -> 1
| _, AddrOf _ -> -1
- | StartOf lv1, StartOf lv2 -> compare_lval lv1 lv2
+ | StartOf lv1, StartOf lv2 -> compare_lval ~strict lv1 lv2
| StartOf _, _ -> 1
| _, StartOf _ -> -1
| Info _, Info _ ->
Cmdline.Kernel_log.fatal
"[exp_compare] Info node is obsolete. Do not use it"
- and compare_lval (h1,o1) (h2,o2) =
- let res = compare_lhost h1 h2 in
- if res = 0 then compare_offset o1 o2 else res
+ and compare_lval ~strict (h1,o1) (h2,o2) =
+ let res = compare_lhost ~strict h1 h2 in
+ if res = 0 then compare_offset ~strict o1 o2 else res
- and compare_lhost h1 h2 =
+ and compare_lhost ~strict h1 h2 =
match h1, h2 with
| Var v1, Var v2 -> Varinfo.compare v1 v2
| Var _, Mem _ -> 1
- | Mem e1, Mem e2 -> compare_exp e1 e2
+ | Mem e1, Mem e2 -> compare_exp ~strict e1 e2
| Mem _, Var _ -> -1
- and compare_offset o1 o2 =
+ and compare_offset ~strict o1 o2 =
match o1, o2 with
| NoOffset, NoOffset -> 0
| NoOffset, _ -> 1
| _, NoOffset -> -1
| Field(f1,o1), Field(f2, o2) ->
let res = Fieldinfo.compare f1 f2 in
- if res = 0 then compare_offset o1 o2 else res
+ if res = 0 then compare_offset ~strict o1 o2 else res
| Field _, _ -> 1
| _, Field _ -> -1
| Index(e1, o1), Index(e2, o2) ->
- let res = compare_exp e1 e2 in
- if res = 0 then compare_offset o1 o2 else res
+ let res = compare_exp ~strict e1 e2 in
+ if res = 0 then compare_offset ~strict o1 o2 else res
let prime = 83047
let rec hash_exp acc e =
@@ -1060,35 +1096,43 @@ module Wide_string =
Datatype.List_with_collections(Datatype.Int64)
(struct let module_name = "Cil_datatype.Wide_string" end)
-module Constant =
+module Constant_input =
struct
let pretty_ref = Extlib.mk_fun "Cil_datatype.Constant.pretty_ref"
- include Make_with_collections
- (struct
- include Datatype.Undefined
- type t = constant
- let name = "Constant"
- let reprs = [ CInt64(Integer.zero, IInt, Some "0") ]
- let compare = compare_constant
- let hash = hash_const
- let equal = Datatype.from_compare
- let pretty fmt t = !pretty_ref fmt t
- end)
+ include Datatype.Serializable_undefined
+ type t = constant
+ let name = "Constant"
+ let reprs = [ CInt64(Integer.zero, IInt, Some "0") ]
+ let compare = compare_constant
+ let hash = hash_const
+ let equal = Datatype.from_compare
+ let pretty fmt t = !pretty_ref fmt t
end
-module ExpStructEq =
- Make_with_collections
- (struct
- include Datatype.Undefined
- type t = exp
- let name = "ExpStructEq"
- let reprs = [ Exp.dummy ]
- let compare = StructEq.compare_exp
- let hash = StructEq.hash_exp 7863
- let equal = Datatype.from_compare
- let pretty fmt t = !Exp.pretty_ref fmt t
- end)
+module Constant = struct
+ include
+ Make_compare_non_strict(Constant_input)
+ let pretty_ref = Constant_input.pretty_ref
+end
+
+module ConstantStrict =
+ Make_compare_strict(Constant_input)
+
+module ExpStructEq_input = struct
+ include Datatype.Serializable_undefined
+ type t = exp
+ let name = "ExpStructEq"
+ let structural_descr = Structural_descr.t_abstract
+ let reprs = [ Exp.dummy ]
+ let compare = StructEq.compare_exp
+ let hash = StructEq.hash_exp 7863
+ let equal = Datatype.from_compare
+ let pretty fmt t = !Exp.pretty_ref fmt t
+end
+
+module ExpStructEq = Make_compare_non_strict(ExpStructEq_input)
let () = compare_exp_struct_eq := ExpStructEq.compare
+module ExpStructEqStrict = Make_compare_strict(ExpStructEq_input)
module Block = struct
let pretty_ref = Extlib.mk_fun "Cil_datatype.Block.pretty_ref"
@@ -1174,20 +1218,24 @@ module Lval = struct
end)
end
-module LvalStructEq =
- Make_with_collections
- (struct
- type t = lval
- let name = "LvalStructEq"
- let reprs = List.map (fun v -> Var v, NoOffset) Varinfo.reprs
- let compare = StructEq.compare_lval
- let equal = Datatype.from_compare
- let hash = StructEq.hash_lval 13598
- let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
- let pretty fmt x = !Lval.pretty_ref fmt x
- let varname _ = "lv"
- end)
+module LvalStructEq_input = struct
+ include Datatype.Serializable_undefined
+ type t = lval
+ let name = "LvalStructEq"
+ let reprs = List.map (fun v -> Var v, NoOffset) Varinfo.reprs
+ let structural_descr = Structural_descr.t_abstract
+ let compare = StructEq.compare_lval
+ let equal = Datatype.from_compare
+ let hash = StructEq.hash_lval 13598
+ let copy = Datatype.undefined
+ let internal_pretty_code = Datatype.undefined
+ let pretty fmt x = !Lval.pretty_ref fmt x
+ let varname _ = "lv"
+end
+
+module LvalStructEq = Make_compare_non_strict(LvalStructEq_input)
+
+module LvalStructEqStrict = Make_compare_strict(LvalStructEq_input)
module Offset = struct
let pretty_ref = ref (fun _ -> assert false)
@@ -1206,20 +1254,23 @@ module Offset = struct
end)
end
-module OffsetStructEq =
- Make_with_collections
- (struct
- type t = offset
- let name = "OffsetStructEq"
- let reprs = [NoOffset]
- let compare = StructEq.compare_offset
- let equal = Datatype.from_compare
- let hash = StructEq.hash_offset 75489
- let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
- let pretty fmt x = !Offset.pretty_ref fmt x
- let varname _ = "offs"
- end)
+module OffsetStructEq_input = struct
+ include Datatype.Serializable_undefined
+ type t = offset
+ let name = "OffsetStructEq"
+ let reprs = [NoOffset]
+ let structural_descr = Structural_descr.t_abstract
+ let compare = StructEq.compare_offset
+ let equal = Datatype.from_compare
+ let hash = StructEq.hash_offset 75489
+ let copy = Datatype.undefined
+ let internal_pretty_code = Datatype.undefined
+ let pretty fmt x = !Offset.pretty_ref fmt x
+ let varname _ = "offs"
+end
+
+module OffsetStructEq = Make_compare_non_strict(OffsetStructEq_input)
+module OffsetStructEqStrict = Make_compare_strict(OffsetStructEq_input)
(**************************************************************************)
(** {3 ACSL types} *)
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index b3e80ccb83eb9781d9bff8923a40a0f92ed82512..a5e968d0bdb612cc05ab9a85817ce9bcb3624e12 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -124,10 +124,21 @@ module Enumitem: S_with_collections_pretty with type t = enumitem
*)
module Wide_string: S_with_collections with type t = int64 list
+
(**
@since Oxygen-20120901
*)
-module Constant: S_with_collections_pretty with type t = constant
+module Constant: sig
+ include S_with_collections with type t = constant
+ val pretty_ref: (Format.formatter -> t -> unit) ref
+end
+
+(**
+ Same as {!Constant}, but comparison is strict, in the sense that it will take
+ into account textual representation if provided.
+ @since Frama-C+dev
+*)
+module ConstantStrict: S_with_collections with type t = constant
(** Note that the equality is based on eid. For structural equality, use
{!ExpStructEq} *)
@@ -138,6 +149,12 @@ end
module ExpStructEq: S_with_collections with type t = exp
+(**
+ structural equality, with strict constant comparison as in {!ConstantStrict}
+ @since Frama-C+dev
+*)
+module ExpStructEqStrict: S_with_collections with type t = exp
+
module Fieldinfo: S_with_collections_pretty with type t = fieldinfo
module File: S with type t = file
@@ -175,6 +192,12 @@ module Lval: S_with_collections_pretty with type t = lval
*)
module LvalStructEq: S_with_collections with type t = lval
+(**
+ structural equality, with strict constant comparison as in {!ConstantStrict}
+ @since Frama-C+dev
+*)
+module LvalStructEqStrict: S_with_collections with type t = lval
+
(** Same remark as for Lval.
For structural equality, use {!OffsetStructEq}. *)
module Offset: S_with_collections_pretty with type t = offset
@@ -182,6 +205,12 @@ module Offset: S_with_collections_pretty with type t = offset
(** @since Oxygen-20120901 *)
module OffsetStructEq: S_with_collections with type t = offset
+(**
+ structural equality, with strict constant comparison as in {!ConstantStrict}
+ @since Frama-C+dev
+*)
+module OffsetStructEqStrict: S_with_collections with type t = offset
+
module Stmt_Id: Hptmap.Id_Datatype with type t = stmt
module Stmt: sig
include S_with_collections_pretty with type t = stmt
diff --git a/src/plugins/value/domains/hcexprs.ml b/src/plugins/value/domains/hcexprs.ml
index b4fa7fa020a46b1932ba121a8e38cfbb284bca91..89c8ddc4839c37947a3910bd7bb58ae1728d0b33 100644
--- a/src/plugins/value/domains/hcexprs.ml
+++ b/src/plugins/value/domains/hcexprs.ml
@@ -22,8 +22,20 @@
open Cil_types
-module Exp = Cil_datatype.ExpStructEq
-module Lval = Cil_datatype.LvalStructEq
+(* The default comparison of Cil_datatype does not distinguish constants
+ with different textual representations in the source code when they
+ represent the same value.
+ However, when option -eva-all-rounding-modes-constants is enabled, the
+ evaluation of floating-point constants may differ according to their
+ textual representation: when the constant is not exactly representable in the
+ floating-point type, an interval is used instead of the nearest singleton
+ value. In this case, two constants with the same nearest value but different
+ textual representation may not be equal. We thus use the [compare_strict]
+ comparison, which also compares the textual representation of constants. *)
+
+module Exp = Cil_datatype.ExpStructEqStrict
+
+module Lval = Cil_datatype.LvalStructEqStrict
(* lvalues are never stored under a constructor [E]. *)
type unhashconsed_exprs = E of Exp.t | LV of Lval.t
diff --git a/tests/float/oracle_equality/dr.2.res.oracle b/tests/float/oracle_equality/dr.2.res.oracle
deleted file mode 100644
index 10fe6f869598523c6f022e1f593f9c0dfd617337..0000000000000000000000000000000000000000
--- a/tests/float/oracle_equality/dr.2.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-27c27
-< [eva] tests/float/dr.i:26: Frama_C_show_each: {0; 1}, {0; 1}
----
-> [eva] tests/float/dr.i:26: Frama_C_show_each: {1}, {0; 1}
-32c32
-< e1 ∈ {0; 1}
----
-> e1 ∈ {1}