diff --git a/src/kernel_services/abstract_interp/cvalue.ml b/src/kernel_services/abstract_interp/cvalue.ml
index 31435f52e940154822a5ed8f287ba3b865d547b1..cd0302182f097efe009c8ea7585809ed908c4857 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 3833510f45385496990a5a6b9c64bed6941a268c..90bfb1924700f4a5b597d6afdd700718f8ded3cc 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 a140b50d5417719f819fe5f58842c6cfdf60c2ab..02b738f217d265bbce854e76e3a1fce580571163 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 1cfd5913f95c4c23ac89d4c09727b4fd282c9317..b07c2784f33df77c2b729de4f62537b93df1baeb 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 7a00272b4718576cefb8ccadfc7d155e0fda2eeb..259619512a643712dac569f0afe21ce46d2b972c 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 20849fc24f13f5c343f93559d3375a2e6d22c563..ab4f7f2bbe235abaace452f428eb7f6508df940c 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 51ae8be9c7d024c802083e0043245a872cd6eba7..ff81ae95980d1cb80f4b7c5c74a1671d38c58788 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 0a6deb04f7ac2eb8ed62b1b44a1ab4444fbeabeb..4035461bb02127f9fe958e4b2916ae069eb37fed 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 5717cc78c7bfb6b68537bb40f4533e52e7101cdd..45e863e4f7981f8a83a75d6314b6f1bd9d1d5068 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 b7bfddf3611be3b582087c74b25e0abcb1a05cdb..195b7d1e8a1e7caeb2356b5fc596332416f69d28 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 a4a6a452f3aff86c13f6cee5a7f8d0787042399a..4716792bf20239e5f966ce524c2fc0026a49c0cc 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 3c854e20979cd4b00b78c8e0ba68de0d8cb206d5..bbef859f5cc8432714302d28fddd6b135145b75d 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 c6c3090b4e82314ba0dd2d30ac3d490d33b1c045..d38208bafd99f815c4b52664507a9172b5f67d4e 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 e83de193e9c8ea97b51ea89c9e9f5643c4e429bd..604a74a6c922bdd4b3628765b9a0eff99e40070d 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 7b3d7628ec4809d974fa4e3f3fae64418ff6d5ef..5a0a99e26e7ad09c73229ea44a40cdfeb221a4c6 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 cc3f46cc428f3142cc69028f82f8ef532f261a14..2a4fee7165a1f9b6cfc7ed44f4fd16ac6d4e5ceb 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 0364f4b0f0ffc9c3c1f98fed02d2ec5c7260b1ca..06e3667bb18ef4bf9f6ade0094ddc3f9fe2f778c 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 2924a23612871f2dbbaa59c831ce7710cbb83180..d721e62e638a22343470bb3815108b0e92ad2ec0 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 950dc8745b371c643e11a8df1865e97798e22982..6ba460b8da9fe1f45b14226d6403a4f8fad23116 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 c174803290531a6985cf538763f9483be7edd2ad..d10d70e06e14cea74be1afc75cf6a0bb78a05593 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 fd6dd002c1fd6a1f11cad1a194f3ba3e26caee81..c54cb15e261c6a79823c7bb6460c4792c2a9a275 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. *)