From b0b5ce920ad6af23f19d1464ab1691cba289a210 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 25 Oct 2023 16:08:49 +0200
Subject: [PATCH] [Eva] Changes the signature of the widening in most cvalue
modules.
- In int_interval, int_val, ival, locations and cvalue: [widen] now takes
optional named arguments [size] and [hint].
- Updates Offsetmap functor accordingly.
- Removes types [numerical_widen_hint] and [size_widen_hint]:
modules only declare one [widen_hint] type.
- Removes module Ival.Widen_hints, and uses Integer.Set directly instead.
---
src/kernel_services/abstract_interp/cvalue.ml | 6 ++---
.../abstract_interp/cvalue.mli | 12 +++------
.../abstract_interp/int_interval.ml | 26 +++++++++---------
.../abstract_interp/int_interval.mli | 8 ++++--
.../abstract_interp/int_val.ml | 9 +++----
.../abstract_interp/int_val.mli | 12 ++++-----
src/kernel_services/abstract_interp/ival.ml | 27 +++++++++----------
src/kernel_services/abstract_interp/ival.mli | 12 ++++-----
src/kernel_services/abstract_interp/lmap.ml | 6 ++---
src/kernel_services/abstract_interp/lmap.mli | 4 +--
.../abstract_interp/locations.ml | 13 +++++----
.../abstract_interp/locations.mli | 8 ++----
.../abstract_interp/offsetmap.ml | 12 ++++-----
.../abstract_interp/offsetmap.mli | 2 +-
.../offsetmap_lattice_with_isotropy.ml | 11 ++++----
.../abstract_interp/widen_type.mli | 4 +--
.../eva/domains/gauges/gauges_domain.ml | 4 +--
.../eva/domains/multidim/multidim_domain.ml | 4 +--
src/plugins/eva/domains/octagons.ml | 7 +----
src/plugins/eva/domains/symbolic_locs.ml | 3 +--
src/plugins/eva/utils/widen.mli | 2 +-
21 files changed, 84 insertions(+), 108 deletions(-)
diff --git a/src/kernel_services/abstract_interp/cvalue.ml b/src/kernel_services/abstract_interp/cvalue.ml
index 31435f52e94..cd0302182f0 100644
--- a/src/kernel_services/abstract_interp/cvalue.ml
+++ b/src/kernel_services/abstract_interp/cvalue.ml
@@ -756,11 +756,9 @@ module V_Or_Uninitialized = struct
(* let (==>) = (fun x y -> (not x) || y) *)
- type size_widen_hint = V.size_widen_hint
- type numerical_widen_hint = V.numerical_widen_hint
type widen_hint = V.widen_hint
- let widen wh t1 t2 =
- create (get_flags t2) (V.widen wh (get_v t1) (get_v t2))
+ let widen ?size ?hint t1 t2 =
+ create (get_flags t2) (V.widen ?size ?hint (get_v t1) (get_v t2))
let equal t1 t2 =
(get_flags t1) = (get_flags t2) &&
diff --git a/src/kernel_services/abstract_interp/cvalue.mli b/src/kernel_services/abstract_interp/cvalue.mli
index 3833510f453..90bfb192470 100644
--- a/src/kernel_services/abstract_interp/cvalue.mli
+++ b/src/kernel_services/abstract_interp/cvalue.mli
@@ -46,13 +46,9 @@ module V : sig
of all of them. Use some shortcuts *)
with type M.t = Location_Bytes.M.t
and type t = Location_Bytes.t
- and type numerical_widen_hint = Location_Bytes.numerical_widen_hint
- and type size_widen_hint = Location_Bytes.size_widen_hint
include Offsetmap_lattice_with_isotropy.S
with type t := t
- and type numerical_widen_hint := numerical_widen_hint
- and type size_widen_hint := size_widen_hint
and type widen_hint := widen_hint
val pretty_typ: Cil_types.typ option -> t Pretty_utils.formatter
@@ -174,9 +170,7 @@ module V_Or_Uninitialized : sig
include Offsetmap_lattice_with_isotropy.S
with type t := t
- and type size_widen_hint = Location_Bytes.size_widen_hint
- and type numerical_widen_hint = Location_Bytes.numerical_widen_hint
- and type widen_hint = Locations.Location_Bytes.widen_hint
+ and type widen_hint = Locations.Location_Bytes.widen_hint
include Lattice_type.With_Under_Approximation with type t:= t
include Lattice_type.With_Narrow with type t := t
include Lattice_type.With_Top with type t := t
@@ -239,7 +233,7 @@ end
module V_Offsetmap: sig
include Offsetmap_sig.S
with type v = V_Or_Uninitialized.t
- and type widen_hint = V_Or_Uninitialized.numerical_widen_hint
+ and type widen_hint = V_Or_Uninitialized.widen_hint
val narrow: t -> t -> t Lattice_bounds.or_bottom
val narrow_reinterpret: t -> t -> t Lattice_bounds.or_bottom
@@ -259,7 +253,7 @@ module Model: sig
include Lmap_sig.S
with type v = V_Or_Uninitialized.t
and type offsetmap = V_Offsetmap.t
- and type widen_hint_base = V_Or_Uninitialized.numerical_widen_hint
+ and type widen_hint_base = V_Or_Uninitialized.widen_hint
include Lattice_type.With_Narrow with type t := t
diff --git a/src/kernel_services/abstract_interp/int_interval.ml b/src/kernel_services/abstract_interp/int_interval.ml
index a140b50d541..02b738f217d 100644
--- a/src/kernel_services/abstract_interp/int_interval.ml
+++ b/src/kernel_services/abstract_interp/int_interval.ml
@@ -330,30 +330,28 @@ let meet t1 t2 =
let narrow = meet
-type size_widen_hint = Integer.t
-type generic_widen_hint = Datatype.Integer.Set.t
-type widen_hint = size_widen_hint * generic_widen_hint
+type widen_hint = Datatype.Integer.Set.t
-let widen (bitsize,wh) t1 t2 =
+let widen ?(size=Integer.zero) ?(hint = Datatype.Integer.Set.empty) t1 t2 =
if equal t1 t2 then t2
else
(* Add possible interval limits deducted from the bitsize *)
- let wh =
+ let thresholds =
(* If bitsize > 128, the values do not correspond to a scalar type.
This can (rarely) happen on structures or arrays that have been
reinterpreted as one value by the offsetmaps. In this case, do not
use limits, and do not create arbitrarily large integers. *)
- if Integer.gt bitsize (Integer.of_int 128)
+ if Integer.gt size (Integer.of_int 128)
then Datatype.Integer.Set.empty
- else if Integer.is_zero bitsize
- then wh
+ else if Integer.is_zero size
+ then hint
else
let limits =
- [ Integer.neg (Integer.two_power (Integer.pred bitsize));
- Integer.pred (Integer.two_power (Integer.pred bitsize));
- Integer.pred (Integer.two_power bitsize); ]
+ Integer.[ neg (two_power (pred size));
+ pred (two_power (pred size));
+ pred (two_power size); ]
in
- Datatype.Integer.Set.(union wh (of_list limits))
+ Datatype.Integer.Set.(union hint (of_list limits))
in
let modu = Int.(pgcd (pgcd t1.modu t2.modu) (abs (sub t1.rem t2.rem))) in
let rem = Int.e_rem t1.rem modu in
@@ -363,7 +361,7 @@ let widen (bitsize,wh) t1 t2 =
| None -> None
| Some min2 ->
try
- let v = Datatype.Integer.Set.nearest_elt_le min2 wh
+ let v = Datatype.Integer.Set.nearest_elt_le min2 thresholds
in Some (Int.round_up_to_r ~r:rem ~modu ~min:v)
with Not_found -> None
in
@@ -373,7 +371,7 @@ let widen (bitsize,wh) t1 t2 =
| None -> None
| Some max2 ->
try
- let v = Datatype.Integer.Set.nearest_elt_ge max2 wh
+ let v = Datatype.Integer.Set.nearest_elt_ge max2 thresholds
in Some (Int.round_down_to_r ~r:rem ~modu ~max:v)
with Not_found -> None
in
diff --git a/src/kernel_services/abstract_interp/int_interval.mli b/src/kernel_services/abstract_interp/int_interval.mli
index 1cfd5913f95..b07c2784f33 100644
--- a/src/kernel_services/abstract_interp/int_interval.mli
+++ b/src/kernel_services/abstract_interp/int_interval.mli
@@ -32,9 +32,13 @@ include Datatype.S_with_collections
include Eva_lattice_type.Full_AI_Lattice_with_cardinality with type t := t
-type widen_hint = Integer.t * Datatype.Integer.Set.t
+(** Hints for the widening: set of relevant thresholds. *)
+type widen_hint = Datatype.Integer.Set.t
-val widen: widen_hint -> t -> t -> t
+(** [widen ~size ~hint t1 t2] is an over-approximation of [join t1 t2].
+ [size] is the size (in bits) of the widened value, [hint] is a set of
+ relevant thresholds for the widened interval bounds. *)
+val widen: ?size:Integer.t -> ?hint:widen_hint -> t -> t -> t
(** Checks that the interval defined by [min, max, rem, modu] is well formed. *)
val check:
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index 7a00272b471..259619512a6 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -30,10 +30,7 @@ let small_cardinal_Int () = Int.of_int (small_cardinal ())
let emitter = Lattice_messages.register "Int_val"
let log_imprecision s = Lattice_messages.emit_imprecision emitter s
-module Widen_Hints = Datatype.Integer.Set
-type size_widen_hint = Integer.t
-type generic_widen_hint = Widen_Hints.t
-type widen_hint = size_widen_hint * generic_widen_hint
+type widen_hint = Datatype.Integer.Set.t
(* --------------------------------- Datatype ------------------------------- *)
@@ -383,14 +380,14 @@ let meet v1 v2 =
let narrow = meet (* meet is exact *)
-let widen widen_hints t1 t2 =
+let widen ?size ?hint t1 t2 =
if equal t1 t2 || cardinal_zero_or_one t1 then t2
else
match t2 with
| Itv _ | Set _ ->
let i1 = make_itv t1
and i2 = make_itv t2 in
- inject_itv (Int_interval.widen widen_hints i1 i2)
+ inject_itv (Int_interval.widen ?size ?hint i1 i2)
let intersects v1 v2 =
match v1, v2 with
diff --git a/src/kernel_services/abstract_interp/int_val.mli b/src/kernel_services/abstract_interp/int_val.mli
index 20849fc24f1..ab4f7f2bbe2 100644
--- a/src/kernel_services/abstract_interp/int_val.mli
+++ b/src/kernel_services/abstract_interp/int_val.mli
@@ -30,15 +30,15 @@ open Lattice_bounds
include Datatype.S_with_collections
-module Widen_Hints = Datatype.Integer.Set
-type size_widen_hint = Integer.t
-type generic_widen_hint = Widen_Hints.t
-
include Eva_lattice_type.Full_AI_Lattice_with_cardinality with type t := t
-type widen_hint = size_widen_hint * generic_widen_hint
+(** Hints for the widening: set of relevant thresholds. *)
+type widen_hint = Datatype.Integer.Set.t
-val widen: widen_hint -> t -> t -> t
+(** [widen ~size ~hint t1 t2] is an over-approximation of [join t1 t2].
+ [size] is the size (in bits) of the widened value, and [hint] is a set of
+ relevant thresholds. *)
+val widen: ?size:Integer.t -> ?hint:widen_hint -> t -> t -> t
val zero: t
val one: t
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 51ae8be9c7d..ff81ae95980 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -95,10 +95,7 @@ end
include Type
-module Widen_Hints = Datatype.Integer.Set
-type size_widen_hint = Integer.t
-type numerical_widen_hint = Widen_Hints.t * Fc_float.Widen_Hints.t
-type widen_hint = size_widen_hint * numerical_widen_hint
+type widen_hint = Datatype.Integer.Set.t * Cil_datatype.Logic_real.Set.t
let hash = function
| Bottom -> 311
@@ -303,7 +300,7 @@ let has_smaller_max_bound t1 t2 =
| Some _, None -> 1
| Some m1, Some m2 -> Int.compare m2 m1
-let widen (bitsize,(wh,fh)) t1 t2 =
+let widen ?size ?hint t1 t2 =
if equal t1 t2 || cardinal_zero_or_one t1 || is_bottom t1 then t2
else
match t2 with
@@ -311,22 +308,24 @@ let widen (bitsize,(wh,fh)) t1 t2 =
| Float f2 ->
let f1 = project_float t1 in
let prec =
- if Integer.equal bitsize (Integer.of_int 32)
- then Float_sig.Single
- else if Integer.equal bitsize (Integer.of_int 64)
- then Float_sig.Double
- else if Integer.equal bitsize (Integer.of_int 128)
- then Float_sig.Long_Double
- else Float_sig.Single
+ match Option.bind size Integer.to_int_opt with
+ | Some 32 -> Float_sig.Single
+ | Some 64 -> Float_sig.Double
+ | Some 128 -> Float_sig.Long_Double
+ | Some _ | None -> Float_sig.Single
in
- inject_float (Fval.widen fh prec f1 f2)
+ let hint =
+ Option.fold hint ~some:snd ~none:Cil_datatype.Logic_real.Set.empty
+ in
+ inject_float (Fval.widen hint prec f1 f2)
| Int i2 ->
let i1 = match t1 with
| Bottom -> assert false
| Int i1 -> i1
| Float _ -> Int_val.top
in
- inject_int (Int_val.widen (bitsize,wh) i1 i2)
+ let hint = Option.map fst hint in
+ inject_int (Int_val.widen ?size ?hint i1 i2)
let meet v1 v2 =
if v1 == v2 then v1 else
diff --git a/src/kernel_services/abstract_interp/ival.mli b/src/kernel_services/abstract_interp/ival.mli
index 0a6deb04f7a..4035461bb02 100644
--- a/src/kernel_services/abstract_interp/ival.mli
+++ b/src/kernel_services/abstract_interp/ival.mli
@@ -39,16 +39,16 @@ type t
and exact operations.
*)
-module Widen_Hints = Datatype.Integer.Set
-type size_widen_hint = Integer.t
-type numerical_widen_hint = Widen_Hints.t * Fc_float.Widen_Hints.t
-
include Datatype.S_with_collections with type t := t
include Lattice_type.Full_AI_Lattice_with_cardinality with type t := t
-type widen_hint = size_widen_hint * numerical_widen_hint
+(** Widening hints: set of relevant integer and floating-point thresholds. *)
+type widen_hint = Datatype.Integer.Set.t * Cil_datatype.Logic_real.Set.t
-val widen : widen_hint -> t -> t -> t
+(** [widen ~size ~hint t1 t2] is an over-approximation of [join t1 t2].
+ [size] is the size (in bits) of the widened value, and [hint] is a set of
+ relevant thresholds. *)
+val widen : ?size:Integer.t -> ?hint:widen_hint -> t -> t -> t
val is_bottom : t -> bool
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 5717cc78c7b..45e863e4f79 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -49,7 +49,7 @@ module Make_LOffset
end)
(Offsetmap: Offsetmap_sig.S
with type v = V.t
- and type widen_hint = V.numerical_widen_hint)
+ and type widen_hint = V.widen_hint)
(Default_offsetmap: Default_offsetmap with type v := V.t
and type offsetmap := Offsetmap.t)
=
@@ -58,7 +58,7 @@ struct
type v = V.t
type offsetmap = Offsetmap.t
- type widen_hint_base = V.numerical_widen_hint
+ type widen_hint_base = V.widen_hint
open Default_offsetmap
@@ -440,7 +440,7 @@ struct
(Hptmap_sig.PersistentCache name) UniversalPredicate
~decide_fast ~decide_fst ~decide_snd ~decide_both
- type widen_hint = Base.Set.t * (Base.t -> V.numerical_widen_hint)
+ type widen_hint = Base.Set.t * (Base.t -> V.widen_hint)
(* Precondition : m1 <= m2 *)
let widen (wh_key_set, wh_hints: widen_hint) m1 m2 =
diff --git a/src/kernel_services/abstract_interp/lmap.mli b/src/kernel_services/abstract_interp/lmap.mli
index b7bfddf3611..195b7d1e8a1 100644
--- a/src/kernel_services/abstract_interp/lmap.mli
+++ b/src/kernel_services/abstract_interp/lmap.mli
@@ -72,12 +72,12 @@ module Make_LOffset
include Lattice_type.With_Top_Opt with type t := t
end)
(Offsetmap: Offsetmap_sig.S with type v = V.t
- and type widen_hint = V.numerical_widen_hint)
+ and type widen_hint = V.widen_hint)
(_: Default_offsetmap with type v := V.t
and type offsetmap := Offsetmap.t):
Lmap_sig.S
with type v = V.t
- and type widen_hint_base = V.numerical_widen_hint
+ and type widen_hint_base = V.widen_hint
and type offsetmap = Offsetmap.t
(*
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index a4a6a452f3a..4716792bf20 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -395,18 +395,17 @@ module Location_Bytes = struct
~decide_both
m1 m2
- type size_widen_hint = Ival.size_widen_hint
- type numerical_widen_hint = Base.t -> Ival.numerical_widen_hint
- type widen_hint = size_widen_hint * numerical_widen_hint
+ type widen_hint = Base.t -> Ival.widen_hint
- let widen (size, wh) =
+ let widen ?size ?hint =
let widen_map =
- let decide k v1 v2 =
+ let decide base v1 v2 =
(* Do not perform size-based widening for pointers. This will only
delay convergence, for no real benefit. The only interesting
bound is the validity. *)
- let size = if Base.equal k Base.null then size else Integer.zero in
- Ival.widen (size, wh k) v1 v2
+ let size = if Base.equal base Base.null then size else None in
+ let hint = Option.map (fun f -> f base) hint in
+ Ival.widen ?size ?hint v1 v2
in
M.join
~cache:Hptmap_sig.NoCache (* No cache, because of wh *)
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index 3c854e20979..bbef859f5cc 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -47,17 +47,13 @@ module Location_Bytes : sig
(** Garbled mix of the addresses in the set *)
| Map of M.t (** Precise set of addresses+offsets *)
- type size_widen_hint = Ival.size_widen_hint
- type numerical_widen_hint = Base.t -> Ival.numerical_widen_hint
- type widen_hint = size_widen_hint * numerical_widen_hint
-
(** Those locations have a lattice structure, including standard operations
such as [join], [narrow], etc. *)
include Lattice_type.AI_Lattice_with_cardinal_one with type t := t
- type widen_hint := widen_hint
+ type widen_hint = Base.t -> Ival.widen_hint
- val widen : widen_hint -> t -> t -> t
+ val widen : ?size:Integer.t -> ?hint:widen_hint -> t -> t -> t
include Datatype.S_with_collections with type t := t
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index c6c3090b4e8..d38208bafd9 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -111,7 +111,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
open Format
type v = V.t
- type widen_hint = V.numerical_widen_hint
+ type widen_hint = V.widen_hint
let empty = Empty
(** All high-level functions of this module must handle a size of 0, in which
@@ -1262,13 +1262,13 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
end
- let widen wh t1 t2 =
+ let widen hint t1 t2 =
(* Due to the way f_aux_merge is designed, we can obtain intervals on which
the two bindings do not verify [is_included v1 v2]. The widening
operations require this, so we correct the arguments here. *)
let widen size v1 v2 =
let v2 = if not (V.is_included v1 v2) then V.join v1 v2 else v2 in
- V.widen (size,wh) v1 v2
+ V.widen ~size ~hint v1 v2
in
let f_widen = f_aux_merge_join widen in
let rec aux t1 t2 =
@@ -2188,10 +2188,8 @@ module FullyIsotropic = struct
let shift_bits ~topify:_ ~offset:_ ~size:_ v = v
let cardinal_zero_or_one _ = false
- let widen _wh _ m = m
- type numerical_widen_hint = unit
- type size_widen_hint = Integer.t
- type widen_hint = size_widen_hint * numerical_widen_hint
+ type widen_hint = unit
+ let widen ?size:_ ?hint:_ _ m = m
end
diff --git a/src/kernel_services/abstract_interp/offsetmap.mli b/src/kernel_services/abstract_interp/offsetmap.mli
index e83de193e9c..604a74a6c92 100644
--- a/src/kernel_services/abstract_interp/offsetmap.mli
+++ b/src/kernel_services/abstract_interp/offsetmap.mli
@@ -27,7 +27,7 @@
module Make (V : Offsetmap_lattice_with_isotropy.S) :
Offsetmap_sig.S
with type v = V.t
- and type widen_hint = V.numerical_widen_hint
+ and type widen_hint = V.widen_hint
(**/**)
(* Exported as Int_Intervals, do not use this module directly *)
diff --git a/src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.ml b/src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.ml
index 7b3d7628ec4..5a0a99e26e7 100644
--- a/src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.ml
+++ b/src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.ml
@@ -26,15 +26,16 @@ open Lattice_type
module type S = sig
- type numerical_widen_hint
- type size_widen_hint = Integer.t
-
include Bounded_Join_Semi_Lattice
include With_Cardinal_One with type t := t
- type widen_hint = size_widen_hint * numerical_widen_hint
+ (** Hints for the widening. *)
+ type widen_hint
- val widen : widen_hint -> t -> t -> t
+ (** [widen ~size ~hint v1 v2] is an over-approximation of [join v1 v2].
+ [size] is the size (in bits) of the widened value, and [hint] is some
+ hint for the widening. *)
+ val widen : ?size:Integer.t -> ?hint:widen_hint -> t -> t -> t
val pretty_typ: Cil_types.typ option -> t Pretty_utils.formatter
diff --git a/src/kernel_services/abstract_interp/widen_type.mli b/src/kernel_services/abstract_interp/widen_type.mli
index cc3f46cc428..2a4fee7165a 100644
--- a/src/kernel_services/abstract_interp/widen_type.mli
+++ b/src/kernel_services/abstract_interp/widen_type.mli
@@ -39,7 +39,7 @@ val pretty : Format.formatter -> t -> unit
(** Define numeric hints for one or all variables ([None]),
for a certain stmt or for all statements ([None]). *)
val num_hints:
- Cil_types.stmt option -> Base.t option -> Ival.Widen_Hints.t -> t
+ Cil_types.stmt option -> Base.t option -> Int_val.widen_hint -> t
(** Define floating hints for one or all variables ([None]),
for a certain stmt or for all statements ([None]). *)
@@ -53,7 +53,7 @@ val var_hints : Cil_types.stmt -> Base.Set.t -> t
{!Cvalue.Model.widen}. *)
val hints_from_keys :
Cil_types.stmt -> t ->
- Base.Set.t * (Base.t -> Locations.Location_Bytes.numerical_widen_hint)
+ Base.Set.t * (Base.t -> Locations.Location_Bytes.widen_hint)
(*
Local Variables:
diff --git a/src/plugins/eva/domains/gauges/gauges_domain.ml b/src/plugins/eva/domains/gauges/gauges_domain.ml
index 0364f4b0f0f..06e3667bb18 100644
--- a/src/plugins/eva/domains/gauges/gauges_domain.ml
+++ b/src/plugins/eva/domains/gauges/gauges_domain.ml
@@ -291,11 +291,9 @@ module G = struct
let decide _ _ _ = assert false in
join ~cache ~symmetric:true ~idempotent:false ~decide
- let empty_wh = Integer.zero, (fun _ -> Ival.Widen_Hints.empty, Fc_float.Widen_Hints.empty)
-
let widen =
let cache = cache_name "MV.widen" in
- let decide _ b1 b2 = Some (Cvalue.V.widen empty_wh b1 b2) in
+ let decide _ b1 b2 = Some (Cvalue.V.widen b1 b2) in
inter ~cache ~symmetric:false ~idempotent:true ~decide
let is_included =
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index 2924a236128..d721e62e638 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -272,9 +272,9 @@ struct
let narrow = fun m1 _m2 -> m1
let join = Memory.join
let smash ~oracle = Memory.join ~oracle:(fun _ -> oracle)
- let widen h =
+ let widen hint =
Memory.widen
- (fun ~size v1 v2 -> Value_or_Uninitialized.widen (size,h) v1 v2)
+ (fun ~size v1 v2 -> Value_or_Uninitialized.widen ~size ~hint v1 v2)
let incr_bound = Memory.incr_bound
let get ~oracle m loc =
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index 950dc8745b3..6ba460b8da9 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -211,12 +211,7 @@ module Arith = struct
let r = narrow x y in
if is_bottom r then `Bottom else `Value r
- let widen =
- let hints = Integer.zero,
- (Ival.Widen_Hints.empty,
- Fc_float.Widen_Hints.default_widen_hints)
- in
- Ival.widen hints
+ let widen = Ival.widen
(* TODO: do not use Ival.top on floating-point value? *)
let project_float ival =
diff --git a/src/plugins/eva/domains/symbolic_locs.ml b/src/plugins/eva/domains/symbolic_locs.ml
index c1748032905..d10d70e06e1 100644
--- a/src/plugins/eva/domains/symbolic_locs.ml
+++ b/src/plugins/eva/domains/symbolic_locs.ml
@@ -52,8 +52,7 @@ module K2V = struct
let cache = Hptmap_sig.NoCache in
let symmetric = false in
let idempotent = true in
- let wh = Integer.zero, (fun _b -> Ival.Widen_Hints.empty, Fc_float.Widen_Hints.empty) in
- let decide _ v1 v2 = Some (V.widen wh v1 v2) in
+ let decide _ v1 v2 = Some (V.widen v1 v2) in
M.inter ~cache ~symmetric ~idempotent ~decide
let _narrow =
diff --git a/src/plugins/eva/utils/widen.mli b/src/plugins/eva/utils/widen.mli
index fd6dd002c1f..c54cb15e261 100644
--- a/src/plugins/eva/utils/widen.mli
+++ b/src/plugins/eva/utils/widen.mli
@@ -27,7 +27,7 @@ open Cil_types
(** [getWidenHints kf s] retrieves the set of widening hints related to
function [kf] and statement [s]. *)
val getWidenHints: kernel_function -> stmt ->
- Base.Set.t * (Base.t -> Locations.Location_Bytes.numerical_widen_hint)
+ Base.Set.t * (Base.t -> Locations.Location_Bytes.widen_hint)
(** Parses all widening hints defined via the widen_hint syntax extension.
The result is memoized for subsequent calls. *)
--
GitLab