diff --git a/src/kernel_services/abstract_interp/float_interval.ml b/src/kernel_services/abstract_interp/float_interval.ml
index 7e733d4faa6e16369e30dd6c34f99b2f9e01b6af..316b5b9b46b352161a3d11ca6d9ac95929166890 100644
--- a/src/kernel_services/abstract_interp/float_interval.ml
+++ b/src/kernel_services/abstract_interp/float_interval.ml
@@ -421,6 +421,13 @@ module Make (F: Float_sig.S) = struct
| FRange.NaN -> Comp.False
| FRange.Itv (_b, _e, nan) -> if nan then Comp.Unknown else Comp.True
+ let is_infinite = function
+ | FRange.NaN -> Comp.False
+ | FRange.Itv (b, e, nan) ->
+ if F.is_infinite b || F.is_infinite e
+ then if Cmp.equal b e && not nan then Comp.True else Comp.Unknown
+ else Comp.False
+
let is_finite = function
| FRange.NaN -> Comp.False
| FRange.Itv (b, e, nan) ->
@@ -444,6 +451,19 @@ module Make (F: Float_sig.S) = struct
| FRange.Itv (b, e, true) ->
if positive then `Value nan else `Value (FRange.inject ~nan:false b e)
+ let backward_is_infinite ~positive prec = function
+ | FRange.NaN as v -> if positive then `Bottom else `Value v
+ | FRange.Itv (b, e, nan) as f ->
+ if positive
+ then
+ match F.is_infinite b, F.is_infinite e with
+ | true, true -> `Value (if nan then FRange.inject ~nan:false b e else f)
+ | true, false -> `Value (FRange.inject ~nan:false b b)
+ | false, true -> `Value (FRange.inject ~nan:false e e)
+ | false, false -> `Bottom
+ else
+ narrow (FRange.add_nan (top_finite prec)) f
+
let backward_is_finite ~positive prec = function
| FRange.NaN as v -> if positive then `Bottom else `Value v
| FRange.Itv (b, e, nan) as f ->
diff --git a/src/kernel_services/abstract_interp/float_interval_sig.mli b/src/kernel_services/abstract_interp/float_interval_sig.mli
index e105e4b09b5f6443989010ae916c880c392d30ef..1ea3e2fcfa2688826eeb7efc269873c7724cd6f0 100644
--- a/src/kernel_services/abstract_interp/float_interval_sig.mli
+++ b/src/kernel_services/abstract_interp/float_interval_sig.mli
@@ -90,8 +90,10 @@ module type S = sig
val is_negative: t -> Abstract_interp.Comp.result
val is_finite: t -> Abstract_interp.Comp.result
+ val is_infinite: t -> Abstract_interp.Comp.result
val is_not_nan: t -> Abstract_interp.Comp.result
val backward_is_finite: positive:bool -> prec -> t -> t or_bottom
+ val backward_is_infinite: positive:bool -> prec -> t -> t or_bottom
val backward_is_nan: positive:bool -> t -> t or_bottom
(** [has_greater_min_bound f1 f2] returns 1 if the interval [f1] has a better
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 2ae8f263be7c99c80cac23faa1cc354cbbb240ed..bc8883d793ffb740fdc3782a05d8b5c328a0fb82 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -737,6 +737,7 @@ let known_logic_funs = [
let known_predicates = [
"\\warning", ACSL;
"\\is_finite", ACSL;
+ "\\is_infinite", ACSL;
"\\is_plus_infinity", ACSL;
"\\is_minus_infinity", ACSL;
"\\is_NaN", ACSL;
@@ -2036,6 +2037,8 @@ let reduce_by_known_papp ~alarm_mode env positive li _labels args =
match li.l_var_info.lv_name, args with
| "\\is_finite", [arg] ->
reduce_float (Fval.backward_is_finite ~positive) arg
+ | "\\is_infinite", [arg] ->
+ reduce_float (Fval.backward_is_infinite ~positive) arg
| "\\is_plus_infinity", [arg] ->
reduce_float (reduce_by_infinity ~pos:true) arg
| "\\is_minus_infinity", [arg] ->
@@ -2555,6 +2558,7 @@ and eval_predicate env pred =
in
match li.l_var_info.lv_name, args with
| "\\is_finite", [arg] -> unary_float Fval.is_finite arg
+ | "\\is_infinite", [arg] -> unary_float Fval.is_infinite arg
| "\\is_plus_infinity", [arg] ->
let pos_inf = Fval.pos_infinity Float_sig.Single in
unary_float (fun f -> Fval.forward_comp Comp.Eq f pos_inf) arg
diff --git a/tests/float/oracle/special_floats.res.oracle b/tests/float/oracle/special_floats.res.oracle
index 653af4625c63f0bc09500f9a1a31b85f3d6c2fba..2cdcf9695086ecd4f8b8ed1fa5aaff28bd1eeb6d 100644
--- a/tests/float/oracle/special_floats.res.oracle
+++ b/tests/float/oracle/special_floats.res.oracle
@@ -8,11 +8,11 @@
global_infinity ∈ {inf}
global_nan ∈ NaN
[eva] computing for function nan_comparisons <- main.
- Called from tests/float/special_floats.c:94.
+ Called from tests/float/special_floats.c:117.
[eva] Recording results for nan_comparisons
[eva] Done for function nan_comparisons
[eva] computing for function is_infinite <- main.
- Called from tests/float/special_floats.c:95.
+ Called from tests/float/special_floats.c:118.
[eva] tests/float/special_floats.c:29: check 'true' got status valid.
[eva:alarm] tests/float/special_floats.c:30: Warning:
check 'false' got status invalid.
@@ -20,53 +20,80 @@
check 'false' got status invalid.
[eva:alarm] tests/float/special_floats.c:32: Warning:
check 'false' got status invalid.
-[eva:alarm] tests/float/special_floats.c:34: Warning:
+[eva:alarm] tests/float/special_floats.c:33: Warning:
check 'false' got status invalid.
-[eva] tests/float/special_floats.c:35: check 'true' got status valid.
-[eva] tests/float/special_floats.c:36: check 'true' got status valid.
-[eva:alarm] tests/float/special_floats.c:37: Warning:
+[eva:alarm] tests/float/special_floats.c:35: Warning:
check 'false' got status invalid.
+[eva] tests/float/special_floats.c:36: check 'true' got status valid.
+[eva] tests/float/special_floats.c:37: check 'true' got status valid.
+[eva] tests/float/special_floats.c:38: check 'true' got status valid.
[eva:alarm] tests/float/special_floats.c:39: Warning:
check 'false' got status invalid.
-[eva] tests/float/special_floats.c:40: check 'true' got status valid.
[eva:alarm] tests/float/special_floats.c:41: Warning:
check 'false' got status invalid.
-[eva:alarm] tests/float/special_floats.c:42: Warning:
+[eva] tests/float/special_floats.c:42: check 'true' got status valid.
+[eva:alarm] tests/float/special_floats.c:43: Warning:
check 'false' got status invalid.
-[eva:alarm] tests/float/special_floats.c:46: Warning:
- assertion got status unknown.
-[eva] tests/float/special_floats.c:47: Frama_C_show_each_pos_infinity: {inf}
+[eva:alarm] tests/float/special_floats.c:44: Warning:
+ check 'false' got status invalid.
+[eva:alarm] tests/float/special_floats.c:45: Warning:
+ check 'false' got status invalid.
+[eva:alarm] tests/float/special_floats.c:49: Warning:
+ check 'unknown' got status unknown.
[eva:alarm] tests/float/special_floats.c:50: Warning:
+ check 'unknown' got status unknown.
+[eva:alarm] tests/float/special_floats.c:51: Warning:
+ check 'unknown' got status unknown.
+[eva:alarm] tests/float/special_floats.c:52: Warning:
+ check 'false' got status invalid.
+[eva:alarm] tests/float/special_floats.c:53: Warning:
+ check 'unknown' got status unknown.
+[eva:alarm] tests/float/special_floats.c:57: Warning:
assertion got status unknown.
-[eva] tests/float/special_floats.c:51: Frama_C_show_each_neg_infinity: {-inf}
-[eva:alarm] tests/float/special_floats.c:54: Warning:
+[eva] tests/float/special_floats.c:58: Frama_C_show_each_pos_infinity: {inf}
+[eva:alarm] tests/float/special_floats.c:61: Warning:
assertion got status unknown.
-[eva:alarm] tests/float/special_floats.c:55: Warning:
+[eva] tests/float/special_floats.c:62: Frama_C_show_each_neg_infinity: {-inf}
+[eva:alarm] tests/float/special_floats.c:65: Warning:
assertion got status unknown.
-[eva] tests/float/special_floats.c:56:
+[eva] tests/float/special_floats.c:66:
+ Frama_C_show_each_infinities: [-inf .. inf]
+[eva:alarm] tests/float/special_floats.c:69: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/float/special_floats.c:70: Warning:
+ assertion got status unknown.
+[eva] tests/float/special_floats.c:71:
+ Frama_C_show_each_finite_nan:
+ [-1.79769313486e+308 .. 1.79769313486e+308] ∪ {NaN}
+[eva:alarm] tests/float/special_floats.c:74: Warning:
+ assertion got status unknown.
+[eva] tests/float/special_floats.c:75:
Frama_C_show_each_finite_nan:
[-1.79769313486e+308 .. 1.79769313486e+308] ∪ {NaN}
-[eva:alarm] tests/float/special_floats.c:59: Warning:
+[eva:alarm] tests/float/special_floats.c:78: Warning:
assertion got status unknown.
-[eva] tests/float/special_floats.c:60:
+[eva] tests/float/special_floats.c:79:
Frama_C_show_each_top: [-inf .. inf] ∪ {NaN}
-[eva:alarm] tests/float/special_floats.c:63: Warning:
+[eva:alarm] tests/float/special_floats.c:82: Warning:
+ assertion got status unknown.
+[eva] tests/float/special_floats.c:83: Frama_C_show_each_pos_infinity: {inf;NaN}
+[eva:alarm] tests/float/special_floats.c:86: Warning:
assertion got status unknown.
-[eva] tests/float/special_floats.c:64: Frama_C_show_each_pos_infinity: {inf;NaN}
+[eva] tests/float/special_floats.c:87: Frama_C_show_each_neg_infinity: {-inf}
[eva] Recording results for is_infinite
[eva] Done for function is_infinite
[eva] computing for function macro_infinity <- main.
- Called from tests/float/special_floats.c:96.
-[eva] tests/float/special_floats.c:74: Frama_C_show_each_infinity: {inf}
-[eva] tests/float/special_floats.c:75: assertion got status valid.
+ Called from tests/float/special_floats.c:119.
+[eva] tests/float/special_floats.c:97: Frama_C_show_each_infinity: {inf}
+[eva] tests/float/special_floats.c:98: assertion got status valid.
[eva] Recording results for macro_infinity
[eva] Done for function macro_infinity
[eva] computing for function macro_nan <- main.
- Called from tests/float/special_floats.c:97.
-[eva] tests/float/special_floats.c:84: Frama_C_show_each_nan: NaN
-[eva] tests/float/special_floats.c:85: assertion got status valid.
-[eva] tests/float/special_floats.c:86: assertion got status valid.
-[eva] tests/float/special_floats.c:87: assertion got status valid.
+ Called from tests/float/special_floats.c:120.
+[eva] tests/float/special_floats.c:107: Frama_C_show_each_nan: NaN
+[eva] tests/float/special_floats.c:108: assertion got status valid.
+[eva] tests/float/special_floats.c:109: assertion got status valid.
+[eva] tests/float/special_floats.c:110: assertion got status valid.
[eva] Recording results for macro_nan
[eva] Done for function macro_nan
[eva] Recording results for main
diff --git a/tests/float/special_floats.c b/tests/float/special_floats.c
index 1e07cd3a6ba385e0b3eec0bda2eb0aa1381200d3..732c2cc3e5814adf905a8ddf711e7188b5749e9b 100644
--- a/tests/float/special_floats.c
+++ b/tests/float/special_floats.c
@@ -28,19 +28,30 @@ void is_infinite () {
double zero = -0.;
/*@ check true: \is_finite(zero); */
/*@ check false: !\is_finite(zero); */
+ /*@ check false: \is_infinite(zero); */
/*@ check false: \is_plus_infinity(zero); */
/*@ check false: \is_minus_infinity(zero); */
double inf = INFINITY;
/*@ check false: \is_finite(inf); */
/*@ check true: !\is_finite(inf); */
+ /*@ check true: \is_infinite(inf); */
/*@ check true: \is_plus_infinity(inf); */
/*@ check false: \is_minus_infinity(inf); */
double nan = NAN;
/*@ check false: \is_finite(nan); */
/*@ check true: !\is_finite(nan); */
+ /*@ check false: \is_infinite(nan); */
/*@ check false: \is_plus_infinity(nan); */
/*@ check false: \is_minus_infinity(nan); */
- double d = any_double;
+ double d;
+ /* Tests the evaluation on imprecise values. */
+ d = rand ? zero : (rand ? -inf : nan);
+ /*@ check unknown: \is_finite(d); */
+ /*@ check unknown: !\is_finite(d); */
+ /*@ check unknown: \is_infinite(d); */
+ /*@ check false: \is_plus_infinity(d); */
+ /*@ check unknown: \is_minus_infinity(d); */
+ d = any_double;
/* Tests the reduction by assertions. */
if (rand) {
/*@ assert \is_plus_infinity(d); */
@@ -50,11 +61,19 @@ void is_infinite () {
/*@ assert \is_minus_infinity(d); */
Frama_C_show_each_neg_infinity(d);
}
+ if (rand) {
+ /*@ assert \is_infinite(d); */
+ Frama_C_show_each_infinities(d);
+ }
if (rand) {
/*@ assert !\is_plus_infinity(d); */
/*@ assert !\is_minus_infinity(d); */
Frama_C_show_each_finite_nan(d);
}
+ if (rand) {
+ /*@ assert !\is_infinite(d); */
+ Frama_C_show_each_finite_nan(d);
+ }
if (rand) {
/*@ assert !\is_finite(d); */
Frama_C_show_each_top(d);
@@ -63,6 +82,10 @@ void is_infinite () {
/*@ assert !\is_finite(d); */
Frama_C_show_each_pos_infinity(d);
}
+ if (d < 0.) {
+ /*@ assert \is_infinite(d); */
+ Frama_C_show_each_neg_infinity(d);
+ }
}
float global_infinity = INFINITY;