diff --git a/src/kernel_services/abstract_interp/fc_float.ml b/src/kernel_services/abstract_interp/fc_float.ml
index 3d0b23e3631f7bfb202e8e67e383728d05b71b8b..58da42b53eed54dfd699c1b3afaa653eff7f601b 100644
--- a/src/kernel_services/abstract_interp/fc_float.ml
+++ b/src/kernel_services/abstract_interp/fc_float.ml
@@ -109,24 +109,60 @@ let prev_float prec f =
then Down >>% fun () -> Floating_point.round_to_single_precision_float f
else f
-let m_pi = 3.1415929794311523 (* single-precision *)
-let m_pi_2 = 1.5707964897155761 (* single-precision *)
-let max_single_precision_float = Floating_point.max_single_precision_float
-
let le f1 f2 = compare f1 f2 <= 0
-let widen_up f =
- if le f (-0.) then -0.
- else if le f 0. then 0.
- else if le f 1. then 1.
- else if le f m_pi_2 then m_pi_2
- else if le f m_pi then m_pi
- else if le f 10. then 10.
- else if le f 1e10 then 1e10
- else if le f max_single_precision_float then max_single_precision_float
- else if le f 1e80 then 1e80
- else if le f max_float then max_float
- else infinity
+
+(* --------------------------------------------------------------------------
+ Widen hints
+ -------------------------------------------------------------------------- *)
+
+module Widen_Hints = struct
+
+ include Datatype.Float.Set
+
+ let pretty fmt s =
+ if not (is_empty s) then
+ Pretty_utils.pp_iter
+ ~pre:"@[<hov 1>{"
+ ~suf:"}@]"
+ ~sep:";@ "
+ iter Floating_point.pretty fmt s
+
+ let of_list l =
+ match l with
+ | [] -> empty
+ | [e] -> singleton e
+ | e :: q ->
+ List.fold_left (fun acc x -> add x acc) (singleton e) q
+
+ let m_pi = 3.1415929794311523 (* single-precision *)
+ let m_pi_2 = 1.5707964897155761 (* single-precision *)
+ let max_single_float = Floating_point.max_single_precision_float
+
+ let default_widen_hints =
+ let l = [0.0;1.0;m_pi_2;m_pi;10.;1e10;max_single_float;1e80] in
+ union (of_list l) (of_list (List.map (fun x -> -. x) l))
+
+end
+
+type widen_hints = Widen_Hints.t
+
+let widen_up wh prec f =
+ let r = try Widen_Hints.nearest_elt_ge f wh
+ with Not_found ->
+ if le f max_float then max_float
+ else infinity
+ in
+ round_to_precision Up prec r
+
+let widen_down wh prec f =
+ let r = try Widen_Hints.nearest_elt_le f wh
+ with Not_found ->
+ if le (-. max_float) f then (-. max_float)
+ else neg_infinity
+ in
+ round_to_precision Down prec r
+
let neg = (~-.)
let abs = abs_float
diff --git a/src/kernel_services/abstract_interp/float_interval.ml b/src/kernel_services/abstract_interp/float_interval.ml
index 89c49bcc1665585e90cd3eb29bd1c4fd622e20d0..13650e1b3183bdf9b665803d79f5d9eb61f90e05 100644
--- a/src/kernel_services/abstract_interp/float_interval.ml
+++ b/src/kernel_services/abstract_interp/float_interval.ml
@@ -314,14 +314,12 @@ module Make (F: Float_sig.S) = struct
| (FRange.NaN, FRange.Itv (b1, e1, _)) -> FRange.inject ~nan:true b1 e1
| FRange.NaN, FRange.NaN -> FRange.nan
- let widen_down f = F.neg (F.widen_up (F.neg f))
-
- let widen f1 f2 =
+ let widen wh prec f1 f2 =
assert (is_included f1 f2);
match f1, f2 with
| FRange.Itv (b1, e1, _), FRange.Itv (b2, e2, nan) ->
- let b = if Cmp.equal b2 b1 then b2 else widen_down b2 in
- let e = if Cmp.equal e2 e1 then e2 else F.widen_up e2 in
+ let b = if Cmp.equal b2 b1 then b2 else F.widen_down wh prec b2 in
+ let e = if Cmp.equal e2 e1 then e2 else F.widen_up wh prec e2 in
(** widen_up and down produce double only if the input is a double *)
FRange.inject ~nan b e
| FRange.NaN, f2 -> f2
diff --git a/src/kernel_services/abstract_interp/float_interval.mli b/src/kernel_services/abstract_interp/float_interval.mli
index 51cb520393b5c50cb8390dadddfdf829c78602ba..66a803c74e15d961e77583d823dfb8e316278630 100644
--- a/src/kernel_services/abstract_interp/float_interval.mli
+++ b/src/kernel_services/abstract_interp/float_interval.mli
@@ -26,3 +26,4 @@
Supports NaN and infinite values. *)
module Make (Float: Float_sig.S) :
Float_interval_sig.S with type float := Float.t
+ and type widen_hints := Float.widen_hints
diff --git a/src/kernel_services/abstract_interp/float_interval_sig.mli b/src/kernel_services/abstract_interp/float_interval_sig.mli
index d2250132fe1b9cf1497adf4cd7b6469ff8e10045..aee6a1d773ce8bba231de5e1445ec9b92131bcba 100644
--- a/src/kernel_services/abstract_interp/float_interval_sig.mli
+++ b/src/kernel_services/abstract_interp/float_interval_sig.mli
@@ -29,6 +29,7 @@ type prec = Float_sig.prec
module type S = sig
type float (** Type of the interval bounds. *)
+ type widen_hints (** Type of the widen hints. *)
type t (** Type of intervals. *)
val packed_descr : Structural_descr.pack
@@ -64,7 +65,7 @@ module type S = sig
val is_included: t -> t -> bool
val join: t -> t -> t
- val widen: t -> t -> t
+ val widen: widen_hints -> prec -> t -> t -> t
val narrow: t -> t -> t or_bottom
val contains_a_zero: t -> bool
diff --git a/src/kernel_services/abstract_interp/float_sig.mli b/src/kernel_services/abstract_interp/float_sig.mli
index 37c9d5be3d16637b75a742a64d47f7914e8b0dc6..5febce60c3dc28d1750d0d3183472ac740a60956 100644
--- a/src/kernel_services/abstract_interp/float_sig.mli
+++ b/src/kernel_services/abstract_interp/float_sig.mli
@@ -30,6 +30,14 @@ type round = Up | Down | Near | Zero
- the ACSL 'real' type. *)
type prec = Single | Double | Long_Double | Real
+
+module type Widen_Hints = sig
+ include FCSet.S with type elt = Datatype.Float.t
+ include Datatype.S with type t:=t
+
+ val default_widen_hints: t
+end
+
module type S = sig
type t
@@ -80,9 +88,14 @@ module type S = sig
behavior as [next_float]. *)
val prev_float: prec -> t -> t
+ module Widen_Hints : Widen_Hints
+ type widen_hints = Widen_Hints.t
+
(** [widen_up f] returns a value strictly larger than [f], such that
- successive applications of [widen_up] converge rapidly to infinity. *)
- val widen_up: t -> t
+ successive applications of [widen_up] converge rapidly to infinity.
+ The first arguments give the set of steps that could be used. *)
+ val widen_up : widen_hints -> prec -> t -> t
+ val widen_down: widen_hints -> prec -> t -> t
(** Floating-point operations. *)
diff --git a/src/kernel_services/abstract_interp/fval.mli b/src/kernel_services/abstract_interp/fval.mli
index 4bebb2da3ebd637dcf68cfed1baf656a8cf5d696..f631b8d354bb7bafacf092ec3d9aa3d35e664be3 100644
--- a/src/kernel_services/abstract_interp/fval.mli
+++ b/src/kernel_services/abstract_interp/fval.mli
@@ -61,6 +61,7 @@ module F : sig
end
include Float_interval_sig.S with type float := F.t
+ and type widen_hints := Fc_float.widen_hints
val round_to_single_precision_float : t -> t
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index eb88284cee5c2e28b1f0e347c0cbfc3208430d4d..3d7cdeb70656b929e2f259a7dcb20977f6eea92b 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -52,8 +52,7 @@ module Widen_Arithmetic_Value_Set = struct
include Datatype.Integer.Set
let pretty fmt s =
- if is_empty s then Format.fprintf fmt "{}"
- else
+ if not (is_empty s) then
Pretty_utils.pp_iter
~pre:"@[<hov 1>{"
~suf:"}@]"
@@ -102,8 +101,8 @@ type t =
module Widen_Hints = Widen_Arithmetic_Value_Set
type size_widen_hint = Integer.t
-type generic_widen_hint = Widen_Hints.t
-type widen_hint = size_widen_hint * generic_widen_hint
+type numerical_widen_hint = Widen_Hints.t * Fc_float.Widen_Hints.t
+type widen_hint = size_widen_hint * numerical_widen_hint
let some_zero = Some Int.zero
@@ -619,13 +618,22 @@ let has_smaller_max_bound t1 t2 =
| Some _, None -> 1
| Some m1, Some m2 -> Int.compare m2 m1
-let widen (bitsize,wh) t1 t2 =
+let widen (bitsize,(wh,fh)) t1 t2 =
if equal t1 t2 || cardinal_zero_or_one t1 then t2
else
match t2 with
| Float f2 ->
let f1 = project_float t1 in
- Float (Fval.widen f1 f2)
+ 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
+ in
+ Float (Fval.widen fh prec f1 f2)
| Top _ | Set _ ->
(* Add possible interval limits deducted from the bitsize *)
let wh =
diff --git a/src/kernel_services/abstract_interp/ival.mli b/src/kernel_services/abstract_interp/ival.mli
index 32218fd774658eb5f127b9d0603a205fd1b8153e..cc7f8630939e8ca2024d3abea7fadb2075d7f635 100644
--- a/src/kernel_services/abstract_interp/ival.mli
+++ b/src/kernel_services/abstract_interp/ival.mli
@@ -58,12 +58,12 @@ module Widen_Hints : sig
end
type size_widen_hint = Integer.t
-type generic_widen_hint = Widen_Hints.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
- and type widen_hint = size_widen_hint * generic_widen_hint
+ and type widen_hint = size_widen_hint * numerical_widen_hint
val is_bottom : t -> bool
val overlaps: partial:bool -> size:Integer.t -> t -> t -> bool
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 825aa7b0b7446d42855c91482a4f1c7d1458fef4..5d1f91af760b0dd01978e7f807f285a33a7f6445 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -38,7 +38,7 @@ module Make_LOffset
end)
(Offsetmap: module type of Offsetmap_sig
with type v = V.t
- and type widen_hint = V.generic_widen_hint)
+ and type widen_hint = V.numerical_widen_hint)
(Default_offsetmap: sig
val name: string
val default_offsetmap : Base.t -> Offsetmap.t Bottom.or_bottom
@@ -50,7 +50,7 @@ struct
type v = V.t
type offsetmap = Offsetmap.t
- type widen_hint_base = V.generic_widen_hint
+ type widen_hint_base = V.numerical_widen_hint
open Default_offsetmap
@@ -432,7 +432,7 @@ struct
(Hptmap_sig.PersistentCache name) UniversalPredicate
~decide_fast ~decide_fst ~decide_snd ~decide_both
- type widen_hint = Base.Set.t * (Base.t -> V.generic_widen_hint)
+ type widen_hint = Base.Set.t * (Base.t -> V.numerical_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 44f39505c5bc96129f0a44021069b449f4c71229..29251098017a421902788ccb53c76f850708758c 100644
--- a/src/kernel_services/abstract_interp/lmap.mli
+++ b/src/kernel_services/abstract_interp/lmap.mli
@@ -39,7 +39,7 @@ module Make_LOffset
end)
(Offsetmap: module type of Offsetmap_sig
with type v = V.t
- and type widen_hint = V.generic_widen_hint)
+ and type widen_hint = V.numerical_widen_hint)
(Default_offsetmap: sig
val name: string
(** Used to create different datatypes each time the functor is applied *)
@@ -72,7 +72,7 @@ module Make_LOffset
end):
module type of Lmap_sig
with type v = V.t
- and type widen_hint_base = V.generic_widen_hint
+ and type widen_hint_base = V.numerical_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 70ca0060d5d777a9a3e5afc27d693aa004b0b1b2..7487068ab5c2ae2c4c61f32ca14f31f7bd570e39 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -405,8 +405,8 @@ module Location_Bytes = struct
m1 m2
type size_widen_hint = Ival.size_widen_hint
- type generic_widen_hint = Base.t -> Ival.generic_widen_hint
- type widen_hint = size_widen_hint * generic_widen_hint
+ type numerical_widen_hint = Base.t -> Ival.numerical_widen_hint
+ type widen_hint = size_widen_hint * numerical_widen_hint
let widen (size, wh) =
let widen_map =
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index 654cd6dbc403b113fa9cacd7d0403f2b4809798b..8ae6ee928ead48cb7b26d60b3cdd0f41474b109c 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -46,8 +46,8 @@ module Location_Bytes : sig
| Map of M.t (** Precise set of addresses+offsets *)
type size_widen_hint = Ival.size_widen_hint
- type generic_widen_hint = Base.t -> Ival.generic_widen_hint
- type widen_hint = size_widen_hint * generic_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. *)
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index bd89eb563c1519850e970cafdb39ef3b69fcbd07..506f4f18d86809dbf22a77df367a7c1aea3f7625 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -108,7 +108,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
open Format
type v = V.t
- type widen_hint = V.generic_widen_hint
+ type widen_hint = V.numerical_widen_hint
let empty = Empty
(** All high-level functions of this module must handle a size of 0, in which
@@ -2194,9 +2194,9 @@ module FullyIsotropic = struct
let cardinal_zero_or_one _ = false
let widen _wh _ m = m
- type generic_widen_hint = unit
+ type numerical_widen_hint = unit
type size_widen_hint = Integer.t
- type widen_hint = size_widen_hint * generic_widen_hint
+ type widen_hint = size_widen_hint * numerical_widen_hint
end
diff --git a/src/kernel_services/abstract_interp/offsetmap.mli b/src/kernel_services/abstract_interp/offsetmap.mli
index 88e2986c36d8cebb73384279ffd563b139a00eb3..7f518453dcb7e02ec3635170439fad134c507e68 100644
--- a/src/kernel_services/abstract_interp/offsetmap.mli
+++ b/src/kernel_services/abstract_interp/offsetmap.mli
@@ -27,7 +27,7 @@
module Make (V : module type of Offsetmap_lattice_with_isotropy) :
module type of Offsetmap_sig
with type v = V.t
- and type widen_hint = V.generic_widen_hint
+ and type widen_hint = V.numerical_widen_hint
(**/**)
(* Exported as Int_Intervals, do not use this module directly *)
diff --git a/src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.mli b/src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.mli
index e2dfef042edd030211d9100ad5ac0ee2819d52f3..5c443aff195ad24d0c66c50121c1acad6af0adcd 100644
--- a/src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.mli
+++ b/src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.mli
@@ -24,11 +24,11 @@
open Lattice_type
-type generic_widen_hint
+type numerical_widen_hint
type size_widen_hint = Integer.t
include Bounded_Join_Semi_Lattice
-include With_Widening with type t := t and type widen_hint = size_widen_hint * generic_widen_hint
+include With_Widening with type t := t and type widen_hint = size_widen_hint * numerical_widen_hint
include With_Cardinal_One with type t := t
val pretty_typ: Cil_types.typ option -> t Pretty_utils.formatter
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 78284d2e1d4a394ff72b29b142cf3d7e439d4830..11b85c2cbe735c3b9ecbf283b83f25d2cc1f3860 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -291,7 +291,7 @@ 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)
+ let empty_wh = Integer.zero, (fun _ -> Ival.Widen_Hints.empty, Fc_float.Widen_Hints.empty)
let widen =
let cache = cache_name "MV.widen" in
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 1d197a22ce9d2aff5f1bef4948b660b9d368ebe9..952cf517636e04216c67d41e5f55e7d0dbc11d26 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -52,7 +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 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
M.inter ~cache ~symmetric ~idempotent ~decide
diff --git a/src/plugins/value/utils/widen.ml b/src/plugins/value/utils/widen.ml
index 2356d40a5625ee76dca0b91c517da77d1160d3e7..94d70a29988d190344d375c4b9d481938bba0eb4 100644
--- a/src/plugins/value/utils/widen.ml
+++ b/src/plugins/value/utils/widen.ml
@@ -34,14 +34,32 @@ let dkey = Widen_hints_ext.dkey
reuse loop indexes...
*)
+let rec constFoldTermToNearestFloat = function
+ | TConst (LReal r) -> Some (r.r_nearest)
+ | TUnOp (Neg,e) -> begin
+ match (constFoldTermToNearestFloat e.term_node) with
+ | None -> None
+ | Some e -> Some (-. e)
+ end
+ | _ -> None
+
class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
inherit Visitor.frama_c_inplace
val widen_hints = init_widen_hints
val enclosing_loops = init_enclosing_loops
- method private add_thresholds ?base thresholds =
- widen_hints := Widen_type.join (Widen_type.num_hints None(*see note*) base thresholds) !widen_hints
+ method private add_int_thresholds ?base int_thresholds =
+ widen_hints :=
+ Widen_type.join
+ (Widen_type.num_hints None(*see note*) base int_thresholds)
+ !widen_hints
+
+ method private add_float_thresholds ?base float_thresholds =
+ widen_hints :=
+ Widen_type.join
+ (Widen_type.float_hints None(*see note*) base float_thresholds)
+ !widen_hints
method private add_var_hints ~stmt hints =
widen_hints := Widen_type.join (Widen_type.var_hints stmt hints) !widen_hints
@@ -63,20 +81,27 @@ class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
"could not interpret loop pragma relative to widening variables"
end
| Widen_hints l -> begin
- let f (lv, lnum, lt) t = match t with
+ let f (lv, lint, lfloat, lt) t = match t with
| { term_node= TLval (TVar { lv_origin = Some vi}, _)} ->
- (Base.of_varinfo vi :: lv, lnum, lt)
+ (Base.of_varinfo vi :: lv, lint, lfloat, lt)
| { term_node= TConst (Integer(v,_))} ->
- (lv, Ival.Widen_Hints.add v lnum, lt)
- | _ -> (lv, lnum, t::lt)
+ (lv, Ival.Widen_Hints.add v lint, lfloat, lt)
+ | _ ->
+ match constFoldTermToNearestFloat t.term_node with
+ | Some f -> (lv, lint, Fc_float.Widen_Hints.add f lfloat, lt)
+ | None -> (lv, lint, lfloat, t::lt)
in
- match List.fold_left f ([], Ival.Widen_Hints.empty, []) l with
- | (vars, thresholds, []) ->
+ match List.fold_left f ([], Ival.Widen_Hints.empty, Fc_float.Widen_Hints.empty, []) l with
+ | (vars, int_thresholds, float_thresholds, []) ->
(* the annotation is empty or contains only variables *)
- if vars = [] then
- self#add_thresholds thresholds
- else
- List.iter (fun base -> self#add_thresholds ~base thresholds) vars
+ if vars = [] then begin
+ self#add_int_thresholds int_thresholds;
+ self#add_float_thresholds float_thresholds
+ end else
+ List.iter (fun base ->
+ self#add_int_thresholds ~base int_thresholds;
+ self#add_float_thresholds ~base float_thresholds;
+ ) vars
| _ ->
Value_parameters.warning ~once:true
"could not interpret loop pragma relative to widening hint"
@@ -137,17 +162,17 @@ class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
match e with
| {enode=(CastE(_, { enode=Lval (Var varinfo, _)})
| Lval (Var varinfo, _))} ->
- let thresholds = Ival.Widen_Hints.singleton Integer.zero in
+ let int_thresholds = Ival.Widen_Hints.singleton Integer.zero in
let base = Base.of_varinfo varinfo in
- self#add_thresholds ~base thresholds;
+ self#add_int_thresholds ~base int_thresholds;
Cil.DoChildren
| _ -> Cil.DoChildren
and comparison_visit add1 add2 e1 e2 =
let add base set =
- let thresholds =
+ let int_thresholds =
List.fold_right Ival.Widen_Hints.add set Ival.Widen_Hints.empty
in
- self#add_thresholds ~base thresholds
+ self#add_int_thresholds ~base int_thresholds
in
let i1, i2 = Cil.constFoldToInt e1, Cil.constFoldToInt e2 in begin
match i1, i2, e1, e2 with
@@ -184,8 +209,8 @@ class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
let add_hint vidx size shift =
let bound1 = Integer.sub size shift in
let bound2 = Integer.(sub bound1 one) in
- let thresholds = Ival.Widen_Hints.of_list [bound1; bound2] in
- self#add_thresholds ~base:(Base.of_varinfo vidx) thresholds
+ let int_thresholds = Ival.Widen_Hints.of_list [bound1; bound2] in
+ self#add_int_thresholds ~base:(Base.of_varinfo vidx) int_thresholds
in
(* Find inside [idx] a variable on which we will add hints. [shift] is an
integer that indicates that we access to [idx+shift], instead of to
@@ -252,6 +277,9 @@ let base_of_static_hvars hvars =
(* syntactic constraints prevent this from happening *)
Value_parameters.fatal "unsupported lhost: %a" Printer.pp_lval (Mem e, offset)
+type threshold = Int_th of Integer.t | Float_th of float
+
+(* try parsing as int, then as float *)
let threshold_of_threshold_term ht =
let global_find_init vi =
try (Globals.Vars.find vi).init with Not_found -> None
@@ -260,16 +288,36 @@ let threshold_of_threshold_term ht =
(new Logic_utils.simplify_const_lval global_find_init) ht
in
match Logic_utils.constFoldTermToInt ht with
- | None -> Value_parameters.abort ~source:(fst ht.term_loc)
- "could not parse widening hint: %a@ \
- If it contains variables, they must be global const integers."
- Printer.pp_term ht
- | Some i -> i
+ | Some i -> Int_th i
+ | None ->
+ match constFoldTermToNearestFloat ht.term_node with
+ | Some f -> Float_th f
+ | None ->
+ Value_parameters.abort ~source:(fst ht.term_loc)
+ "could not parse widening hint: %a@ \
+ If it contains variables, they must be global const integers."
+ Printer.pp_term ht
let thresholds_of_threshold_terms hts =
- List.fold_left (fun acc' ht ->
- Ival.Widen_Hints.add (threshold_of_threshold_term ht) acc'
- ) Ival.Widen_Hints.empty hts
+ let has_int = ref false in
+ let has_float = ref false in
+ List.fold_left (fun (int_acc, float_acc) ht ->
+ match threshold_of_threshold_term ht with
+ | Int_th i ->
+ if !has_float then
+ Value_parameters.abort ~source:(fst ht.term_loc)
+ "widening hint mixing integers and floats: %a"
+ Printer.pp_term ht;
+ has_int := true;
+ Ival.Widen_Hints.add i int_acc, float_acc
+ | Float_th f ->
+ if !has_int then
+ Value_parameters.abort ~source:(fst ht.term_loc)
+ "widening hint mixing integers and floats: %a"
+ Printer.pp_term ht;
+ has_float := true;
+ int_acc, Fc_float.Widen_Hints.add f float_acc
+ ) (Ival.Widen_Hints.empty, Fc_float.Widen_Hints.empty) hts
class hints_visitor init_widen_hints global = object(self)
inherit Visitor.frama_c_inplace
@@ -284,17 +332,27 @@ class hints_visitor init_widen_hints global = object(self)
List.iter
(fun ({Widen_hints_ext.vars; loc}, wh_terms) ->
let base = base_of_static_hvars vars in
- let thresholds = thresholds_of_threshold_terms wh_terms in
+ let int_thresholds, float_thresholds =
+ thresholds_of_threshold_terms wh_terms
+ in
Value_parameters.feedback ~source:(fst loc) ~dkey
- "adding%s hint from annotation: %a, %a (for all statements)"
+ "adding%s hint from annotation: %a, %t (for all statements)"
(if global then " global" else "")
(Pretty_utils.pp_opt ~none:(format_of_string "for all variables")
Base.pretty) base
- Ival.Widen_Hints.pretty thresholds;
- let new_hints =
- Widen_type.num_hints None (* see note above *) base thresholds
+ (fun fmt ->
+ if Ival.Widen_Hints.is_empty int_thresholds then
+ Format.fprintf fmt "float:%a" Fc_float.Widen_Hints.pretty float_thresholds
+ else
+ Ival.Widen_Hints.pretty fmt int_thresholds);
+ let new_int_hints =
+ Widen_type.num_hints None (* see note above *) base int_thresholds
+ in
+ widen_hints := Widen_type.join new_int_hints !widen_hints;
+ let new_float_hints =
+ Widen_type.float_hints None (* see note above *) base float_thresholds
in
- widen_hints := Widen_type.join new_hints !widen_hints
+ widen_hints := Widen_type.join new_float_hints !widen_hints
) static_hints
method! vstmt s =
@@ -363,7 +421,8 @@ type dynamic_hint = {
(* dynamic, used to detect when a new base needs to be added to the global
widening hints *);
lv : exp * offset; (* static, parsed once from the AST *)
- thresholds : Ival.Widen_Hints.t; (* static, computed only once *)
+ int_thresholds : Ival.Widen_Hints.t; (* static, computed only once *)
+ float_thresholds : Fc_float.Widen_Hints.t; (* static, computed only once *)
}
module ExpOffset = Datatype.Pair(Exp)(Offset)
@@ -376,13 +435,16 @@ module DynamicHintDatatype = Datatype.Make(struct
Structural_descr.t_tuple
[| Base.Hptset.packed_descr;
ExpOffset.packed_descr;
- Ival.Widen_Hints.packed_descr |]
+ Ival.Widen_Hints.packed_descr;
+ Fc_float.Widen_Hints.packed_descr |]
let reprs =
- List.map
- (fun wh -> { bases = Base.Hptset.empty;
- lv = (Exp.dummy, NoOffset);
- thresholds = wh })
+ Extlib.product
+ (fun wh fh -> { bases = Base.Hptset.empty;
+ lv = (Exp.dummy, NoOffset);
+ int_thresholds = wh;
+ float_thresholds = fh })
Ival.Widen_Hints.reprs
+ Fc_float.Widen_Hints.reprs
let mem_project = Datatype.never_any_project
end)
@@ -430,8 +492,11 @@ let extract_dynamic_hints stmt =
let open Widen_hints_ext in
match hlv.vars with
| HintMem (e, offset) ->
- let thresholds = thresholds_of_threshold_terms threshold_terms in
- { bases = Base.Hptset.empty; lv = (e, offset); thresholds; } :: l
+ let int_thresholds, float_thresholds =
+ thresholds_of_threshold_terms threshold_terms
+ in
+ let bases = Base.Hptset.empty in
+ { bases; lv = (e, offset); int_thresholds; float_thresholds; } :: l
| _-> l
in
List.fold_left aux [] wh
@@ -489,13 +554,18 @@ let dynamic_widen_hints_hook (stmt, _callstack, states) =
let new_hints =
Base.Hptset.fold (fun base acc ->
Value_parameters.debug ~source ~dkey
- "adding new base due to dynamic widen hint: %a, %a"
+ "adding new base due to dynamic widen hint: %a, %a%a"
Base.pretty base
- Ival.Widen_Hints.pretty dhint.thresholds;
- let hint_for_base =
- Widen_type.num_hints None (Some base) dhint.thresholds
+ Ival.Widen_Hints.pretty dhint.int_thresholds
+ Fc_float.Widen_Hints.pretty dhint.float_thresholds;
+ let int_hint_for_base =
+ Widen_type.num_hints None (Some base) dhint.int_thresholds
+ in
+ let float_hint_for_base =
+ Widen_type.float_hints None (Some base) dhint.float_thresholds
in
- Widen_type.join acc hint_for_base
+ let acc = Widen_type.join acc int_hint_for_base in
+ Widen_type.join acc float_hint_for_base
) new_bases acc_hints
in
dhint.bases <- Base.Hptset.union dhint.bases new_bases;
diff --git a/src/plugins/value/utils/widen.mli b/src/plugins/value/utils/widen.mli
index 283459456db5881ad44fa1aeef2dd4be2f6ed06c..b9dc1c6f77b55918273f0fac16cae1a21b5a410b 100644
--- a/src/plugins/value/utils/widen.mli
+++ b/src/plugins/value/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.generic_widen_hint)
+ Base.Set.t * (Base.t -> Locations.Location_Bytes.numerical_widen_hint)
(** Parses all widening hints defined via the widen_hint syntax extension.
The result is memoized for subsequent calls. *)
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index fd1b472fbcca009b6b9a6e26401e81fed87f8346..56124a5079b644189247e11c29afd8807e7ae581 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -744,7 +744,7 @@ module V_Or_Uninitialized = struct
(* let (==>) = (fun x y -> (not x) || y) *)
type size_widen_hint = V.size_widen_hint
- type generic_widen_hint = V.generic_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))
diff --git a/src/plugins/value_types/cvalue.mli b/src/plugins/value_types/cvalue.mli
index 050be2bc75fa411d4c3a971f1c5366e597aac08c..83a60eeb36294f517b7505332afaddb14c46c4de 100644
--- a/src/plugins/value_types/cvalue.mli
+++ b/src/plugins/value_types/cvalue.mli
@@ -46,12 +46,12 @@ 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 generic_widen_hint = Location_Bytes.generic_widen_hint
+ and type numerical_widen_hint = Location_Bytes.numerical_widen_hint
and type size_widen_hint = Location_Bytes.size_widen_hint
include module type of Offsetmap_lattice_with_isotropy
with type t := t
- and type generic_widen_hint := generic_widen_hint
+ and type numerical_widen_hint := numerical_widen_hint
and type size_widen_hint := size_widen_hint
and type widen_hint := widen_hint
@@ -175,7 +175,7 @@ module V_Or_Uninitialized : sig
include module type of Offsetmap_lattice_with_isotropy
with type t := t
and type size_widen_hint = Location_Bytes.size_widen_hint
- and type generic_widen_hint = Location_Bytes.generic_widen_hint
+ and type numerical_widen_hint = Location_Bytes.numerical_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
@@ -237,7 +237,7 @@ module V_Or_Uninitialized : sig
module V_Offsetmap: sig
include module type of Offsetmap_sig
with type v = V_Or_Uninitialized.t
- and type widen_hint = V_Or_Uninitialized.generic_widen_hint
+ and type widen_hint = V_Or_Uninitialized.numerical_widen_hint
val narrow: t -> t -> t Bottom.Type.or_bottom
val narrow_reinterpret: t -> t -> t Bottom.Type.or_bottom
@@ -257,7 +257,7 @@ module Model: sig
include module type of Lmap_sig
with type v = V_Or_Uninitialized.t
and type offsetmap = V_Offsetmap.t
- and type widen_hint_base = V_Or_Uninitialized.generic_widen_hint
+ and type widen_hint_base = V_Or_Uninitialized.numerical_widen_hint
include Lattice_type.With_Narrow with type t := t
diff --git a/src/plugins/value_types/widen_type.ml b/src/plugins/value_types/widen_type.ml
index ed9929b21d0917513bdb7f8b466769f415639d33..157b11f55c9f05d26593a6acb2d63bd061852448 100644
--- a/src/plugins/value_types/widen_type.ml
+++ b/src/plugins/value_types/widen_type.ml
@@ -23,25 +23,36 @@
open Cil_datatype
module Num_hints_stmt = Stmt.Map.Make(Ival.Widen_Hints)
+module Float_hints_stmt = Stmt.Map.Make(Fc_float.Widen_Hints)
module Num_hints_bases = Base.Map.Make(Ival.Widen_Hints)
+module Float_hints_bases = Base.Map.Make(Fc_float.Widen_Hints)
module Num_hints_bases_stmt = Stmt.Map.Make(Num_hints_bases)
+module Float_hints_bases_stmt = Stmt.Map.Make(Float_hints_bases)
module Priority_bases_stmt = Stmt.Map.Make(Base.Set)
type widen_hints = {
priority_bases: Base.Set.t Stmt.Map.t;
default_hints: Ival.Widen_Hints.t;
+ default_float_hints: Fc_float.Widen_Hints.t;
default_hints_by_stmt: Ival.Widen_Hints.t Stmt.Map.t;
+ default_float_hints_by_stmt: Fc_float.Widen_Hints.t Stmt.Map.t;
hints_by_addr: Ival.Widen_Hints.t Base.Map.t;
+ float_hints_by_addr: Fc_float.Widen_Hints.t Base.Map.t;
hints_by_addr_by_stmt: Ival.Widen_Hints.t Base.Map.t Stmt.Map.t;
+ float_hints_by_addr_by_stmt: Fc_float.Widen_Hints.t Base.Map.t Stmt.Map.t;
}
(* an [empty] set of hints *)
let empty = {
priority_bases = Stmt.Map.empty;
default_hints = Ival.Widen_Hints.empty;
+ default_float_hints = Fc_float.Widen_Hints.empty;
default_hints_by_stmt = Stmt.Map.empty;
+ default_float_hints_by_stmt = Stmt.Map.empty;
hints_by_addr = Base.Map.empty;
+ float_hints_by_addr = Base.Map.empty;
hints_by_addr_by_stmt = Stmt.Map.empty;
+ float_hints_by_addr_by_stmt = Stmt.Map.empty;
}
include Datatype.Make(struct
@@ -52,18 +63,27 @@ include Datatype.Make(struct
Structural_descr.t_tuple
[| Priority_bases_stmt.packed_descr;
Ival.Widen_Hints.packed_descr;
+ Fc_float.Widen_Hints.packed_descr;
Num_hints_stmt.packed_descr;
+ Float_hints_stmt.packed_descr;
Num_hints_bases.packed_descr;
- Num_hints_bases_stmt.packed_descr |]
+ Float_hints_bases.packed_descr;
+ Num_hints_bases_stmt.packed_descr;
+ Float_hints_bases_stmt.packed_descr |]
let reprs =
- List.map
- (fun wh ->
- { priority_bases = Stmt.Map.empty;
- default_hints = wh;
- default_hints_by_stmt = Stmt.Map.empty;
- hints_by_addr = Base.Map.empty;
- hints_by_addr_by_stmt = Stmt.Map.empty})
- Ival.Widen_Hints.reprs
+ Extlib.product
+ (fun wh fh ->
+ { priority_bases = Stmt.Map.empty;
+ default_hints = wh;
+ default_float_hints = fh;
+ default_hints_by_stmt = Stmt.Map.empty;
+ default_float_hints_by_stmt = Stmt.Map.empty;
+ hints_by_addr = Base.Map.empty;
+ float_hints_by_addr = Base.Map.empty;
+ float_hints_by_addr_by_stmt = Stmt.Map.empty;
+ hints_by_addr_by_stmt = Stmt.Map.empty
+ })
+ Ival.Widen_Hints.reprs Fc_float.Widen_Hints.reprs
let mem_project = Datatype.never_any_project
end)
@@ -79,17 +99,30 @@ let join wh1 wh2 =
wh1.priority_bases wh2.priority_bases;
default_hints =
Ival.Widen_Hints.union wh1.default_hints wh2.default_hints;
+ default_float_hints =
+ Fc_float.Widen_Hints.union wh1.default_float_hints wh2.default_float_hints;
default_hints_by_stmt =
Stmt.Map.merge (fun _key -> map_merge Ival.Widen_Hints.union)
wh1.default_hints_by_stmt wh2.default_hints_by_stmt;
+ default_float_hints_by_stmt =
+ Stmt.Map.merge (fun _key -> map_merge Fc_float.Widen_Hints.union)
+ wh1.default_float_hints_by_stmt wh2.default_float_hints_by_stmt;
hints_by_addr =
Base.Map.merge (fun _key -> map_merge Ival.Widen_Hints.union)
wh1.hints_by_addr wh2.hints_by_addr;
+ float_hints_by_addr =
+ Base.Map.merge (fun _key -> map_merge Fc_float.Widen_Hints.union)
+ wh1.float_hints_by_addr wh2.float_hints_by_addr;
hints_by_addr_by_stmt =
Stmt.Map.merge (fun _key ->
map_merge (Base.Map.merge
(fun _key -> map_merge Ival.Widen_Hints.union)))
wh1.hints_by_addr_by_stmt wh2.hints_by_addr_by_stmt;
+ float_hints_by_addr_by_stmt =
+ Stmt.Map.merge (fun _key ->
+ map_merge (Base.Map.merge
+ (fun _key -> map_merge Fc_float.Widen_Hints.union)))
+ wh1.float_hints_by_addr_by_stmt wh2.float_hints_by_addr_by_stmt;
}
let pretty fmt wh =
@@ -110,19 +143,32 @@ let pretty fmt wh =
Format.fprintf fmt
"@[priority bases: %a@\n\
default_hints: %a@\n\
+ default_float_hints: %a@\n\
default_hints_by_stmt: %a@\n\
+ default_float_hints_by_stmt: %a@\n\
hints_by_addr: %a@\n\
- hints_by_addr_by_stmt: %a@]"
+ float_hints_by_addr: %a@\n\
+ hints_by_addr_by_stmt: %a@\n\
+ float_hints_by_addr_by_stmt: %a@]"
(pp_bindings pp_stmt Base.Set.pretty) (Stmt.Map.bindings wh.priority_bases)
Ival.Widen_Hints.pretty wh.default_hints
+ Fc_float.Widen_Hints.pretty wh.default_float_hints
(Pretty_utils.pp_list ~sep:",@ "
(Pretty_utils.pp_pair ~sep:" -> " pp_stmt Ival.Widen_Hints.pretty))
(Stmt.Map.bindings wh.default_hints_by_stmt)
+ (Pretty_utils.pp_list ~sep:",@ "
+ (Pretty_utils.pp_pair ~sep:" -> " pp_stmt Fc_float.Widen_Hints.pretty))
+ (Stmt.Map.bindings wh.default_float_hints_by_stmt)
(Pretty_utils.pp_list ~sep:",@ "
(Pretty_utils.pp_pair ~sep:" -> " Base.pretty Ival.Widen_Hints.pretty))
(Base.Map.bindings wh.hints_by_addr)
+ (Pretty_utils.pp_list ~sep:",@ "
+ (Pretty_utils.pp_pair ~sep:" -> " Base.pretty Fc_float.Widen_Hints.pretty))
+ (Base.Map.bindings wh.float_hints_by_addr)
(pp_bindings pp_stmt (pp_base_map Ival.Widen_Hints.pretty))
(Stmt.Map.bindings wh.hints_by_addr_by_stmt)
+ (pp_bindings pp_stmt (pp_base_map Fc_float.Widen_Hints.pretty))
+ (Stmt.Map.bindings wh.float_hints_by_addr_by_stmt)
let hints_for_base default_hints hints_by_base b =
let widen_hints_null =
@@ -147,7 +193,7 @@ let hints_for_base default_hints hints_by_base b =
)
let hints_from_keys stmt h =
- let hints_by_base =
+ let int_hints_by_base =
try
let at_stmt = Stmt.Map.find stmt h.hints_by_addr_by_stmt in
Base.Map.merge (fun _b os1 os2 ->
@@ -158,17 +204,40 @@ let hints_from_keys stmt h =
) at_stmt h.hints_by_addr
with Not_found -> h.hints_by_addr
in
+ let float_hints_by_base =
+ try
+ let at_stmt = Stmt.Map.find stmt h.float_hints_by_addr_by_stmt in
+ Base.Map.merge (fun _b os1 os2 ->
+ match os1, os2 with
+ | Some s1, Some s2 -> Some (Fc_float.Widen_Hints.union s1 s2)
+ | Some s, None | None, Some s -> Some s
+ | None, None -> None
+ ) at_stmt h.float_hints_by_addr
+ with Not_found -> h.float_hints_by_addr
+ in
let prio =
try Stmt.Map.find stmt h.priority_bases
with Not_found -> Base.Set.empty
in
- let default =
+ let int_default =
try
let at_stmt = Stmt.Map.find stmt h.default_hints_by_stmt in
Ival.Widen_Hints.union h.default_hints at_stmt
with Not_found -> h.default_hints
in
- prio, (fun b -> hints_for_base default hints_by_base b)
+ let float_default =
+ try
+ let at_stmt = Stmt.Map.find stmt h.default_float_hints_by_stmt in
+ Fc_float.Widen_Hints.union h.default_float_hints at_stmt
+ with Not_found -> h.default_float_hints
+ in
+ let float_hints_for_base b =
+ try Fc_float.Widen_Hints.union (Base.Map.find b float_hints_by_base) float_default
+ with Not_found -> float_default
+ in
+ prio, (fun b b' ->
+ hints_for_base int_default int_hints_by_base b b',
+ float_hints_for_base b)
let var_hints stmt prio_bases =
{ empty with priority_bases = Stmt.Map.singleton stmt prio_bases }
@@ -185,10 +254,23 @@ let num_hints stmto baseo hints =
| None, None -> (* Hints for all bases and all statements *)
{ empty with default_hints = hints }
+let float_hints stmto baseo hints =
+ match stmto, baseo with
+ | None, Some b -> (* Hints for a base at all statements *)
+ { empty with float_hints_by_addr = Base.Map.singleton b hints }
+ | Some stmt, Some b -> (* Hints for a base at a statement *)
+ { empty with float_hints_by_addr_by_stmt = Stmt.Map.singleton stmt
+ (Base.Map.singleton b hints) }
+ | Some stmt, None -> (* Hints for all bases and a given statement *)
+ { empty with default_float_hints_by_stmt = Stmt.Map.singleton stmt hints }
+ | None, None -> (* Hints for all bases and all statements *)
+ { empty with default_float_hints = hints }
+
(* default set of hints. Depends on the machdep *)
let default () =
- let default = Ival.Widen_Hints.default_widen_hints in
- num_hints None None default
+ let int_default = Ival.Widen_Hints.default_widen_hints in
+ let float_default = Fc_float.Widen_Hints.default_widen_hints in
+ join (num_hints None None int_default) (float_hints None None float_default)
(*
Local Variables:
diff --git a/src/plugins/value_types/widen_type.mli b/src/plugins/value_types/widen_type.mli
index e017c3c17f7aab7600aeca22737eac6b22f8001c..00f9cf979a0e89617a2853ec5f8de1f76be70d9a 100644
--- a/src/plugins/value_types/widen_type.mli
+++ b/src/plugins/value_types/widen_type.mli
@@ -41,6 +41,11 @@ val pretty : Format.formatter -> t -> unit
val num_hints:
Cil_types.stmt option -> Base.t option -> Ival.Widen_Hints.t -> t
+(** Define floating hints for one or all variables ([None]),
+ for a certain stmt or for all statements ([None]). *)
+val float_hints:
+ Cil_types.stmt option -> Base.t option -> Fc_float.Widen_Hints.t -> t
+
(** Define a set of bases to widen in priority for a given statement. *)
val var_hints : Cil_types.stmt -> Base.Set.t -> t
@@ -48,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.generic_widen_hint)
+ Base.Set.t * (Base.t -> Locations.Location_Bytes.numerical_widen_hint)
(*
Local Variables:
diff --git a/tests/misc/oracle/widen_hints_float.res.oracle b/tests/misc/oracle/widen_hints_float.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1b5726f1922996fa5305e1cbde175f5d7d882b14
--- /dev/null
+++ b/tests/misc/oracle/widen_hints_float.res.oracle
@@ -0,0 +1,61 @@
+[kernel] Parsing tests/misc/widen_hints_float.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] computing for function Frama_C_double_interval <- main.
+ Called from tests/misc/widen_hints_float.c:12.
+[eva] using specification for function Frama_C_double_interval
+[eva] tests/misc/widen_hints_float.c:12:
+ function Frama_C_double_interval: precondition 'finite' got status valid.
+[eva] tests/misc/widen_hints_float.c:12:
+ function Frama_C_double_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_double_interval
+[eva] tests/misc/widen_hints_float.c:15: starting to merge loop iterations
+[eva] computing for function Frama_C_double_interval <- main.
+ Called from tests/misc/widen_hints_float.c:19.
+[eva] tests/misc/widen_hints_float.c:19:
+ function Frama_C_double_interval: precondition 'finite' got status valid.
+[eva] tests/misc/widen_hints_float.c:19:
+ function Frama_C_double_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_double_interval
+[eva] tests/misc/widen_hints_float.c:22: starting to merge loop iterations
+[eva] computing for function Frama_C_double_interval <- main.
+ Called from tests/misc/widen_hints_float.c:26.
+[eva] tests/misc/widen_hints_float.c:26:
+ function Frama_C_double_interval: precondition 'finite' got status valid.
+[eva] tests/misc/widen_hints_float.c:26:
+ function Frama_C_double_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_double_interval
+[eva] tests/misc/widen_hints_float.c:28: starting to merge loop iterations
+[eva:alarm] tests/misc/widen_hints_float.c:29: Warning:
+ non-finite double value.
+ assert
+ \is_finite((double)((double)(f3 - (double)64) * (double)(f3 - (double)64)));
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ Frama_C_entropy_source ∈ [--..--]
+ f1 ∈ [-0. .. 71.]
+ f2 ∈ [-80. .. 0.]
+ f3 ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ __retres ∈ {0}
+[from] Computing for function main
+[from] Computing for function Frama_C_double_interval <-main
+[from] Done for function Frama_C_double_interval
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_double_interval:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; min; max
+[from] Function main:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM \nothing
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main:
+ Frama_C_entropy_source; f1; i; f2; i_0; f3; i_1; __retres
+[inout] Inputs for function main:
+ Frama_C_entropy_source
diff --git a/tests/misc/widen_hints_float.c b/tests/misc/widen_hints_float.c
new file mode 100644
index 0000000000000000000000000000000000000000..a0e5a550a5c4e69bb5a6db4def23ba1ac80b4bf0
--- /dev/null
+++ b/tests/misc/widen_hints_float.c
@@ -0,0 +1,33 @@
+#include "__fc_builtin.h"
+
+int main() {
+
+ /*
+ The expression is a parabola p
+ where p([0.;64.]) = [0.;64.] and p([64.;128.]) = [0.;64.].
+ For any value x<0, p(x) < x;
+ For any value 128.<x, p(x) < -x;
+ */
+
+ double f1 = Frama_C_double_interval(0.,1./64.);
+
+ //@ loop widen_hints f1, 71.;
+ for(int i = 0; i < 100; i++){
+ f1 = (64*64 - (f1 - 64) * (f1 - 64))/64;
+ }
+
+ double f2 = Frama_C_double_interval(-1./64.,-0);
+
+ //@ loop widen_hints f2, -80.;
+ for(int i = 0; i < 100; i++){
+ f2 = -(64*64 - (-f2 - 64) * (-f2 - 64))/64;
+ }
+
+ double f3 = Frama_C_double_interval(0.,1./64.);
+
+ for(int i = 0; i < 100; i++){
+ f3 = (64*64 - (f3 - 64) * (f3 - 64))/64;
+ }
+
+ return 0;
+}