diff --git a/share/libc/math.h b/share/libc/math.h
index ff121459534bd3d364ed3040fdf1fd591e60cf11..ad1d732027ff5741d8137ab0f3adf98945ddb396 100644
--- a/share/libc/math.h
+++ b/share/libc/math.h
@@ -37,10 +37,6 @@ typedef double double_t;
#define MATH_ERRNO 1
#define MATH_ERREXCEPT 2
-#define HUGE_VAL 0x1.0p2047
-#define HUGE_VALF 0x1.0p255f
-#define HUGE_VALL 0x1.0p32767L
-
/* The constants below are not part of C99/C11 but they are defined in POSIX */
#define M_E 0x1.5bf0a8b145769p1 /* e */
#define M_LOG2E 0x1.71547652b82fep0 /* log_2 e */
@@ -755,6 +751,37 @@ extern int __finite(double d);
# define isfinite(x) \
(sizeof (x) == sizeof (float) ? __finitef (x) : __finite (x))
+//The (integer x) argument is just here because a function without argument is
+//applied differently in ACSL and C
+
+/*@
+
+ logic float __fc_infinity(integer x) = \plus_infinity;
+ logic float __fc_nan(integer x) = \NaN;
+
+ @*/
+
+/*@
+ ensures \eq_float(\result,\plus_infinity);
+ assigns \result \from \nothing;
+ @*/
+extern const float __fc_infinity(int x);
+
+/*@
+ ensures \is_NaN(\result);
+ assigns \result \from \nothing;
+ @*/
+extern const float __fc_nan();
+
+
+#define INFINITY __fc_infinity(0)
+#define NAN __fc_nan(0)
+
+#define HUGE_VALF INFINITY
+#define HUGE_VAL ((double)INFINITY)
+#define HUGE_VALL ((long double)INFINITY)
+
+
__END_DECLS
__POP_FC_STDLIB
diff --git a/src/kernel_internals/typing/logic_builtin.ml b/src/kernel_internals/typing/logic_builtin.ml
index ae1a73a97132d659383b01a7ec8643a7f72c002d..7bf6f33d929adccfc01553e0efea752412d41cd2 100644
--- a/src/kernel_internals/typing/logic_builtin.ml
+++ b/src/kernel_internals/typing/logic_builtin.ml
@@ -285,6 +285,9 @@ let init =
["m", rounding_mode; "x", Lreal], float_type;
"\\round_double", [],
["m", rounding_mode ; "x", Lreal], double_type;
+ "\\plus_infinity", [], [], float_type;
+ "\\minus_infinity", [], [], float_type;
+ "\\NaN", [], [], float_type;
(*"\\round_quad", [],
["m", rounding_mode; "x", Lreal], long_double_type;*)
diff --git a/src/kernel_services/abstract_interp/float_interval.ml b/src/kernel_services/abstract_interp/float_interval.ml
index 13650e1b3183bdf9b665803d79f5d9eb61f90e05..57dc208681a05f887f6c270fb581898e6ba948ef 100644
--- a/src/kernel_services/abstract_interp/float_interval.ml
+++ b/src/kernel_services/abstract_interp/float_interval.ml
@@ -223,7 +223,7 @@ module Make (F: Float_sig.S) = struct
let pos_zero prec = singleton (Cst.pos_zero prec)
let one prec = singleton (F.of_float Near prec 1.)
let pos_infinity prec = singleton (Cst.pos_infinity prec)
- let _neg_infinity prec = singleton (Cst.neg_infinity prec)
+ let neg_infinity prec = singleton (Cst.neg_infinity prec)
let minus_one_one prec ~nan =
FRange.inject ~nan (F.of_float Near prec (-1.)) (F.of_float Near prec 1.)
@@ -420,6 +420,20 @@ 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_pos_infinity = function
+ | FRange.NaN -> Comp.False
+ | FRange.Itv (b, e, _) ->
+ if not (Cmp.is_pos_infinity e) then Comp.False
+ else if not (Cmp.is_pos_infinity b) then Comp.Unknown
+ else Comp.True
+
+ let is_neg_infinity = function
+ | FRange.NaN -> Comp.False
+ | FRange.Itv (b, e, _) ->
+ if not (Cmp.is_neg_infinity b) then Comp.False
+ else if not (Cmp.is_neg_infinity e) then Comp.Unknown
+ else Comp.True
+
let is_finite = function
| FRange.NaN -> Comp.False
| FRange.Itv (b, e, nan) ->
@@ -441,6 +455,11 @@ module Make (F: Float_sig.S) = struct
| FRange.NaN -> `Bottom
| FRange.Itv (b, e, _) -> `Value (FRange.inject ~nan:false b e)
+ let backward_is_nan = function
+ | FRange.Itv (_, _, false) -> `Bottom
+ | FRange.Itv (_, _, true)
+ | FRange.NaN -> `Value nan
+
let backward_is_finite prec = function
| FRange.NaN -> `Bottom
| FRange.Itv (b, e, _) 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 aee6a1d773ce8bba231de5e1445ec9b92131bcba..fe24f048e452c055057c8b912ad2d275a7a26d1b 100644
--- a/src/kernel_services/abstract_interp/float_interval_sig.mli
+++ b/src/kernel_services/abstract_interp/float_interval_sig.mli
@@ -47,6 +47,10 @@ module type S = sig
(** The NaN singleton *)
val nan: t
+ (** The infinities singleton *)
+ val pos_infinity: prec -> t
+ val neg_infinity: prec -> t
+
(** [inject ~nan b e] creates the floating-point interval [b..e], plus NaN
if [nan] is true. [b] and [e] must be ordered, and not NaN. They can be
infinite. *)
@@ -87,8 +91,11 @@ module type S = sig
val is_finite: t -> Abstract_interp.Comp.result
val is_not_nan: t -> Abstract_interp.Comp.result
+ val is_pos_infinity: t -> Abstract_interp.Comp.result
+ val is_neg_infinity: t -> Abstract_interp.Comp.result
val backward_is_finite: prec -> t -> t or_bottom
val backward_is_not_nan: t -> t or_bottom
+ val backward_is_nan: t -> t or_bottom
(** [has_greater_min_bound f1 f2] returns 1 if the interval [f1] has a better
minimum bound (i.e. greater) than the interval [f2]. *)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index ce9a20a55a312fa437321e4c9a52affec6a9aa2e..f5e973e525dd461f18bf36ac3eeecf5453a9bfbe 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -633,6 +633,9 @@ let known_logic_funs = [
"\\sign", ACSL;
"\\min", ACSL;
"\\max", ACSL;
+ "\\plus_infinity", ACSL;
+ "\\minus_infinity", ACSL;
+ "\\NaN", ACSL;
]
let known_predicates = [
"\\warning", ACSL;
@@ -745,6 +748,16 @@ let rec eval_term ~alarm_mode env t =
(* Special case for the constants \pi and \e. *)
| TLval (TVar {lv_name = "\\pi"}, _) -> ereal (V.inject_float Fval.pi)
| TLval (TVar {lv_name = "\\e"}, _) -> ereal (V.inject_float Fval.e)
+ | TLval (TVar {lv_name = "\\plus_infinity"}, _) ->
+ let v = Cvalue.V.inject_float (Fval.pos_infinity Float_sig.Single) in
+ { etype = Cil.floatType; eunder = v; eover = v; ldeps = empty_logic_deps }
+ | TLval (TVar {lv_name = "\\minus_infinity"}, _) ->
+ let v = Cvalue.V.inject_float (Fval.neg_infinity Float_sig.Single) in
+ { etype = Cil.floatType; eunder = v; eover = v; ldeps = empty_logic_deps }
+ | TLval (TVar {lv_name = "\\NaN"}, _) ->
+ let v = Cvalue.V.inject_float Fval.nan in
+ { etype = Cil.floatType; eunder = v; eover = v; ldeps = empty_logic_deps }
+
| TLval _ ->
let lval = eval_tlval ~alarm_mode env t in
let typ = lval.etype in
@@ -1220,6 +1233,7 @@ and eval_tif : 'a. (alarm_mode:_ -> _ -> _ -> 'a eval_result) -> ('a -> 'a -> 'a
| false, false -> assert false (* a logic alarm would have been raised*)
(* if you add something here, update known_logic_funs above also *)
+(* Constants are directly in eval_terms *)
and eval_known_logic_function ~alarm_mode env li labels args =
let lvi = li.l_var_info in
match lvi.lv_name, li.l_type, labels, args with
@@ -1271,7 +1285,6 @@ and eval_known_logic_function ~alarm_mode env li labels args =
| "\\max", Some Lreal, _, [t1; t2] ->
let backward = Cvalue.V.backward_comp_float_left_true Comp.Ge Fval.Real in
eval_extremum Cil.doubleType backward ~alarm_mode env t1 t2
-
| _ -> assert false
and eval_float_builtin_arity2 ~alarm_mode env name arg1 arg2 =
@@ -1694,6 +1707,7 @@ let reduce_by_left_relation ~alarm_mode env positive tl rel tr =
let debug = false in
if debug then Format.printf "#Left term %a@." Printer.pp_term tl;
let typ_loc, locs = eval_term_as_exact_locs ~alarm_mode env tl in
+ if debug then Format.printf "HERE@.";
let reduce = Eval_op.backward_comp_left_from_type typ_loc in
let rtl = eval_term ~alarm_mode env tr in
let cond_v = rtl.eover in
@@ -1747,40 +1761,40 @@ let rec reduce_by_relation ~alarm_mode env positive t1 rel t2 =
May raise LogicEvalError or Not_an_exact_loc, when no reduction can be done,
and Reduce_to_bottom, in which case the reduction leads to bottom. *)
let reduce_by_known_papp ~alarm_mode env positive li _labels args =
- match positive, li.l_var_info.lv_name, args with
- | true, "\\is_finite", [arg]
- | false, "\\is_NaN", [arg] -> begin
- let fval_reduce =
- (* positive is true for is_finite, false for is_NaN. *)
- if positive
- then Fval.backward_is_finite
- else (fun _fkind -> Fval.backward_is_not_nan)
- in
- try
- let alarm_mode = alarm_reduce_mode () in
- let typ_loc, locs = eval_term_as_exact_locs ~alarm_mode env arg in
- let aux loc env =
- let state = env_current_state env in
- let v = find_or_alarm ~alarm_mode state loc in
- let v = Cvalue_forward.reinterpret typ_loc v in
- let v = match Cil.unrollType typ_loc with
- | TFloat (fkind,_) -> begin
- let v = Cvalue.V.project_float v in
- let kind = Fval.kind fkind in
- match fval_reduce kind v with
- | `Value f -> V.inject_float f
- | `Bottom -> V.bottom
- end
- | _ -> (* Better safe than sorry, we may have e.g. en int location
- here *)
- raise Not_an_exact_loc
- in
- let state' = Cvalue.Model.reduce_previous_binding state loc v in
- overwrite_current_state env state'
+ let reduce_float fval_reduce arg =
+ try
+ let alarm_mode = alarm_reduce_mode () in
+ let typ_loc, locs = eval_term_as_exact_locs ~alarm_mode env arg in
+ let aux loc env =
+ let state = env_current_state env in
+ let v = find_or_alarm ~alarm_mode state loc in
+ let v = Cvalue_forward.reinterpret typ_loc v in
+ let v = match Cil.unrollType typ_loc with
+ | TFloat (fkind,_) -> begin
+ let v = Cvalue.V.project_float v in
+ let kind = Fval.kind fkind in
+ match fval_reduce kind v with
+ | `Value f -> V.inject_float f
+ | `Bottom -> V.bottom
+ end
+ | _ -> (* Better safe than sorry, we may have e.g. en int location
+ here *)
+ raise Not_an_exact_loc
in
- Eval_op.apply_on_all_locs aux locs env
- with Cvalue.V.Not_based_on_null -> env
- end
+ let state' = Cvalue.Model.reduce_previous_binding state loc v in
+ overwrite_current_state env state'
+ in
+ Eval_op.apply_on_all_locs aux locs env
+ with LogicEvalError _ | Not_an_exact_loc | Cvalue.V.Not_based_on_null ->
+ env
+ in
+ match positive, li.l_var_info.lv_name, args with
+ | true, "\\is_finite", [arg] ->
+ reduce_float Fval.backward_is_finite arg
+ | false, "\\is_NaN", [arg] ->
+ reduce_float (fun _fkind -> Fval.backward_is_not_nan) arg
+ | true, "\\is_NaN", [arg] ->
+ reduce_float (fun _fkind -> Fval.backward_is_nan) arg
| _ , ("\\eq_float" | "\\eq_double"), [t1;t2] ->
reduce_by_relation ~alarm_mode env positive t1 Req t2
| _ , ("\\ne_float" | "\\ne_double"), [t1;t2] ->
@@ -2289,6 +2303,8 @@ and eval_predicate env pred =
Value_parameters.abort
"Wrong argument: \\warning expects a constant string"
end
+ | "\\is_plus_infinity", [arg] -> unary_float Fval.is_pos_infinity arg
+ | "\\is_minus_infinity", [arg] -> unary_float Fval.is_neg_infinity arg
| "\\subset", [argl;argr] -> begin
try
let l = eval_term ~alarm_mode env argl in
diff --git a/tests/value/INFINITY_NAN.c b/tests/value/INFINITY_NAN.c
new file mode 100644
index 0000000000000000000000000000000000000000..7b12350993d730cad7ea2414cb85298617a5a444
--- /dev/null
+++ b/tests/value/INFINITY_NAN.c
@@ -0,0 +1,39 @@
+/* run.config*
+ STDOPT: +"-warn-special-float none"
+*/
+
+#include <math.h>
+
+int main1(){
+ float infinity_f = INFINITY;
+ Frama_C_show_each(infinity_f);
+ /*@ assert \eq_float(infinity_f,INFINITY); @*/
+ double infinity_d = HUGE_VAL;
+ if(infinity_f == infinity_d) {
+ return 1;
+ } else {
+ /*@ assert \false; @*/
+ return 0;
+ }
+}
+
+
+volatile float nondet;
+
+int main2(){
+ float nan_f = nondet;
+ Frama_C_show_each(nan_f);
+ /*@ assert \is_NaN(nan_f); @*/
+ double infinity_d = HUGE_VAL;
+ if(nan_f == infinity_d) {
+ /*@ assert \false; @*/
+ return 0;
+ } else {
+ return 1;
+ }
+}
+
+
+int main(){
+ return (main1 () && main2 ());
+}
diff --git a/tests/value/oracle/INFINITY_NAN.res.oracle b/tests/value/oracle/INFINITY_NAN.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d18e3877a6ccd75da4ce8ce953bdeec0fa09f912
--- /dev/null
+++ b/tests/value/oracle/INFINITY_NAN.res.oracle
@@ -0,0 +1,6 @@
+[eva] Warning: Unknown message key summary
+[kernel] Parsing tests/value/INFINITY_NAN.c (with preprocessing)
+[kernel] tests/value/INFINITY_NAN.c:8: Failure: Cannot resolve variable INFINITY
+[kernel] User Error: stopping on file "tests/value/INFINITY_NAN.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.