diff --git a/share/libc/math.h b/share/libc/math.h
index ff121459534bd3d364ed3040fdf1fd591e60cf11..e8b81c90b83c350b1c1b52aa643198aab7e41c8f 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 result_is_infinity: \is_plus_infinity(\result);
+ assigns \result \from \nothing;
+ @*/
+extern const float __fc_infinity(int x);
+
+/*@
+ ensures result_is_nan: \is_NaN(\result);
+ assigns \result \from \nothing;
+ @*/
+extern const float __fc_nan(int x);
+
+
+#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/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 7ba8fa5f2a6c9d5a93c9bfb429456bfaac0b816b..3137c53e5a21baab52734c1af0bbd3abc3009467 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -6899,6 +6899,19 @@ and doExp local_env
"Invalid call to builtin_expect"
end
+ | "__fc_infinity" -> begin
+ piscall := false;
+ let cst = CReal (infinity, FFloat, Some "INFINITY") in
+ pres := Cil.new_exp ~loc (Const cst);
+ prestype := Cil.floatType;
+ end
+ | "__fc_nan" -> begin
+ piscall := false;
+ let cst = CReal (nan, FFloat, Some "NAN") in
+ pres := Cil.new_exp ~loc (Const cst);
+ prestype := Cil.floatType;
+ end
+
(* TODO: Only keep the side effects of the 1st or 2nd argument
| "__builtin_choose_expr" ->
begin match !pargs with
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..a881b71694746b3f6618aa9965359110d8a2ec4a 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.)
@@ -437,17 +437,27 @@ module Make (F: Float_sig.S) = struct
| FRange.Itv (_, _, true)
| FRange.NaN -> Comp.Unknown
- let backward_is_not_nan = function
- | FRange.NaN -> `Bottom
- | FRange.Itv (b, e, _) -> `Value (FRange.inject ~nan:false b e)
-
- let backward_is_finite prec = function
- | FRange.NaN -> `Bottom
- | FRange.Itv (b, e, _) as f ->
- if Cmp.equal b e && F.is_infinite b
- then `Bottom (* [f] is exactly an infinite, we can return `Bottom even
- in the [Real] case *)
- else narrow (top_finite prec) f
+ let backward_is_nan ~positive = function
+ | FRange.NaN as v -> if positive then `Value v else `Bottom
+ | FRange.Itv (_, _, false) as v -> if positive then `Bottom else `Value v
+ | FRange.Itv (b, e, true) ->
+ if positive then `Value nan else `Value (FRange.inject ~nan:false b e)
+
+ 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 ->
+ if positive
+ then
+ if Cmp.equal b e && F.is_infinite b
+ then `Bottom (* [f] is exactly an infinite, we can return `Bottom
+ even in the [Real] case. *)
+ else narrow (top_finite prec) f
+ else
+ match F.is_infinite b, F.is_infinite e with
+ | true, true -> `Value f (* No possible reduction. *)
+ | true, false -> `Value (FRange.inject ~nan b b)
+ | false, true -> `Value (FRange.inject ~nan e e)
+ | false, false -> if nan then `Value FRange.nan else `Bottom
let has_greater_min_bound t1 t2 =
match t1, t2 with
diff --git a/src/kernel_services/abstract_interp/float_interval_sig.mli b/src/kernel_services/abstract_interp/float_interval_sig.mli
index aee6a1d773ce8bba231de5e1445ec9b92131bcba..53b9ae7ec2ed45f0d647612c340d210cb3648ba7 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,8 @@ module type S = sig
val is_finite: t -> Abstract_interp.Comp.result
val is_not_nan: 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_finite: 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
minimum bound (i.e. greater) than the interval [f2]. *)
diff --git a/src/plugins/report/tests/report/oracle/csv.csv b/src/plugins/report/tests/report/oracle/csv.csv
index 18a0e92bcf745d267e58b4a630a8962646e626ed..c44a659ed70c59996a52187b9e77c2f1e8253048 100644
--- a/src/plugins/report/tests/report/oracle/csv.csv
+++ b/src/plugins/report/tests/report/oracle/csv.csv
@@ -1,5 +1,5 @@
directory file line function property kind status property
-FRAMAC_SHARE/libc math.h 526 pow precondition Unknown finite_logic_res: \is_finite(pow(x, y))
+FRAMAC_SHARE/libc math.h 522 pow precondition Unknown finite_logic_res: \is_finite(pow(x, y))
tests/report csv.c 11 main1 signed_overflow Unknown -2147483648 ≤ x * x
tests/report csv.c 11 main1 signed_overflow Unknown x * x ≤ 2147483647
tests/report csv.c 12 main1 index_bound Unknown 0 ≤ x
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 35f3c5c6ac8f1294f13ae513e625884ac38f6d30..089f3c93a5eadaca570d79802bec072a5d689b64 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -446,9 +446,13 @@ let einteger v =
(* Note: some reals cannot be exactly represented as floats; in which
case we do not know their under-approximation. *)
-let ereal v =
+let efloating_point etype fval =
+ let v = V.inject_float fval in
let eunder = under_from_over v in
- { etype = Cil.doubleType; eunder; eover = v; ldeps = empty_logic_deps }
+ { etype; eunder; eover = v; ldeps = empty_logic_deps }
+
+let ereal = efloating_point Cil.doubleType
+let efloat = efloating_point Cil.floatType
let is_true = function
| `True | `TrueReduced _ -> true
@@ -637,6 +641,8 @@ let known_logic_funs = [
let known_predicates = [
"\\warning", ACSL;
"\\is_finite", ACSL;
+ "\\is_plus_infinity", ACSL;
+ "\\is_minus_infinity", ACSL;
"\\is_NaN", ACSL;
"\\eq_float", ACSL;
"\\ne_float", ACSL;
@@ -719,11 +725,14 @@ let rec eval_term ~alarm_mode env t =
| _ -> ast_error "non-evaluable constant")
| TConst (LChr c) ->
einteger (Cvalue.V.inject_int (Cil.charConstToInt c))
- | TConst (LReal { r_lower ; r_upper }) -> begin
- let r_lower = Fval.F.of_float r_lower in
- let r_upper = Fval.F.of_float r_upper in
- let f = Fval.inject Fval.Real r_lower r_upper in
- ereal (V.inject_ival (Ival.inject_float f))
+ | TConst (LReal { r_nearest; r_lower ; r_upper }) -> begin
+ if Fc_float.is_nan r_nearest
+ then ereal Fval.nan
+ else
+ let r_lower = Fval.F.of_float r_lower in
+ let r_upper = Fval.F.of_float r_upper in
+ let f = Fval.inject Fval.Real r_lower r_upper in
+ ereal f
end
(* | TConst ((CStr | CWstr) Missing cases *)
@@ -742,9 +751,15 @@ let rec eval_term ~alarm_mode env t =
eunder = loc_bits_to_loc_bytes_under r.eunder;
eover = loc_bits_to_loc_bytes r.eover }
- (* 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)
+ (* Special case for the constants \pi, \e, \infinity and \NaN. *)
+ | TLval (TVar {lv_name = "\\pi"}, _) -> ereal Fval.pi
+ | TLval (TVar {lv_name = "\\e"}, _) -> ereal Fval.e
+ | TLval (TVar {lv_name = "\\plus_infinity"}, _) ->
+ efloat Fval.(pos_infinity Single)
+ | TLval (TVar {lv_name = "\\minus_infinity"}, _) ->
+ efloat Fval.(neg_infinity Single)
+ | TLval (TVar {lv_name = "\\NaN"}, _) -> efloat Fval.nan
+
| TLval _ ->
let lval = eval_tlval ~alarm_mode env t in
let typ = lval.etype in
@@ -1271,7 +1286,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 =
@@ -1747,53 +1761,67 @@ 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'
+ (* If the term [arg] is a floating-point lvalue with an exact location,
+ reduces its value in [env] by using the backward propagator on fval
+ [fval_reduce]. *)
+ let reduce_float fval_reduce arg =
+ try
+ 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
- | _ , ("\\eq_float" | "\\eq_double"), [t1;t2] ->
+ 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 Cvalue.V.Not_based_on_null -> env
+ in
+ (* Reduces [f] to positive or negative infinity (according to [pos]),
+ or to the complement if [positive] is false. *)
+ let reduce_by_infinity ~pos prec f =
+ let inf = if pos then Fval.pos_infinity prec else Fval.neg_infinity prec in
+ let fval =
+ if positive
+ then inf
+ else Fval.(join nan (join (Fval.neg inf) (top_finite prec)))
+ in
+ Fval.narrow fval f
+ in
+ match li.l_var_info.lv_name, args with
+ | "\\is_finite", [arg] ->
+ reduce_float (Fval.backward_is_finite ~positive) arg
+ | "\\is_plus_infinity", [arg] ->
+ reduce_float (reduce_by_infinity ~pos:true) arg
+ | "\\is_minus_infinity", [arg] ->
+ reduce_float (reduce_by_infinity ~pos:false) arg
+ | "\\is_NaN", [arg] ->
+ reduce_float (fun _fkind -> Fval.backward_is_nan ~positive) arg
+ | ("\\eq_float" | "\\eq_double"), [t1;t2] ->
reduce_by_relation ~alarm_mode env positive t1 Req t2
- | _ , ("\\ne_float" | "\\ne_double"), [t1;t2] ->
+ | ("\\ne_float" | "\\ne_double"), [t1;t2] ->
reduce_by_relation ~alarm_mode env positive t1 Rneq t2
- | _ , ("\\lt_float" | "\\lt_double"), [t1;t2] ->
+ | ("\\lt_float" | "\\lt_double"), [t1;t2] ->
reduce_by_relation ~alarm_mode env positive t1 Rlt t2
- | _ , ("\\le_float" | "\\le_double"), [t1;t2] ->
+ | ("\\le_float" | "\\le_double"), [t1;t2] ->
reduce_by_relation ~alarm_mode env positive t1 Rle t2
- | _ , ("\\gt_float" | "\\gt_double"), [t1;t2] ->
+ | ("\\gt_float" | "\\gt_double"), [t1;t2] ->
reduce_by_relation ~alarm_mode env positive t1 Rgt t2
- | _ , ("\\ge_float" | "\\ge_double"), [t1;t2] ->
+ | ("\\ge_float" | "\\ge_double"), [t1;t2] ->
reduce_by_relation ~alarm_mode env positive t1 Rge t2
- | true, "\\subset", [argl;argr] ->
+ | "\\subset", [argl;argr] when positive ->
let alarm_mode = alarm_reduce_mode () in
let vr = (eval_term ~alarm_mode env argr).eover in
let _typ, locsl = eval_term_as_exact_locs ~alarm_mode env argl in
@@ -2274,6 +2302,12 @@ 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_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
+ | "\\is_minus_infinity", [arg] ->
+ let neg_inf = Fval.neg_infinity Float_sig.Single in
+ unary_float (fun f -> Fval.forward_comp Comp.Eq f neg_inf) arg
| "\\is_NaN", [arg] -> inv_truth (unary_float Fval.is_not_nan arg)
| ("\\eq_float" | "\\eq_double"), [arg1;arg2] -> fval_cmp Comp.Eq arg1 arg2
| ("\\ne_float" | "\\ne_double"), [arg1;arg2] -> fval_cmp Comp.Ne arg1 arg2
diff --git a/src/plugins/value/values/cvalue_forward.ml b/src/plugins/value/values/cvalue_forward.ml
index 81f7f5347720eb559045328300b58485b67d2e40..92edcb72aae965853432a24d2f97c0c99cc88c35 100644
--- a/src/plugins/value/values/cvalue_forward.ml
+++ b/src/plugins/value/values/cvalue_forward.ml
@@ -206,8 +206,8 @@ let assume_not_nan ~assume_finite fkind v =
let kind = Fval.kind fkind in
let evaluate, backward_propagate =
if assume_finite
- then Fval.is_finite, Fval.backward_is_finite
- else Fval.is_not_nan, fun _fkind -> Fval.backward_is_not_nan
+ then Fval.is_finite, Fval.backward_is_finite ~positive:true
+ else Fval.is_not_nan, fun _fkind -> Fval.backward_is_nan ~positive:false
in
match Cvalue.V.project_float v with
| exception Cvalue.V.Not_based_on_null ->
@@ -470,28 +470,31 @@ let make_volatile ?typ v =
else v
let eval_float_constant f fkind fstring =
- let fl, fu = match fstring with
- | Some string when fkind = Cil_types.FLongDouble ||
- Value_parameters.AllRoundingModesConstants.get () ->
- let open Floating_point in
- let {f_lower; f_upper} = snd (parse string) in
- (* Computations are done in double. For long double constants, if we
- reach infinity, we must use the interval [max_double..infty] to be
- sound. Here we even use [-infty..infty]. *)
- if Fc_float.is_infinite f_lower && Fc_float.is_infinite f_upper
- then
- begin
- Value_util.warning_once_current
- "cannot parse floating-point constant, returning imprecise result";
- neg_infinity, infinity
- end
- else f_lower, f_upper
- | None | Some _ -> f, f
- in
- let fl = Fval.F.of_float fl
- and fu = Fval.F.of_float fu in
- let af = Fval.inject (Fval.kind fkind) fl fu in
- V.inject_float af
+ if Fc_float.is_nan f
+ then V.inject_float Fval.nan
+ else
+ let fl, fu = match fstring with
+ | Some string when fkind = Cil_types.FLongDouble ||
+ Value_parameters.AllRoundingModesConstants.get () ->
+ let open Floating_point in
+ let {f_lower; f_upper} = snd (parse string) in
+ (* Computations are done in double. For long double constants, if we
+ reach infinity, we must use the interval [max_double..infty] to be
+ sound. Here we even use [-infty..infty]. *)
+ if Fc_float.is_infinite f_lower && Fc_float.is_infinite f_upper
+ then
+ begin
+ Value_util.warning_once_current
+ "cannot parse floating-point constant, returning imprecise result";
+ neg_infinity, infinity
+ end
+ else f_lower, f_upper
+ | None | Some _ -> f, f
+ in
+ let fl = Fval.F.of_float fl
+ and fu = Fval.F.of_float fu in
+ let af = Fval.inject (Fval.kind fkind) fl fu in
+ V.inject_float af
(*
diff --git a/tests/float/oracle/special_floats.res.oracle b/tests/float/oracle/special_floats.res.oracle
index ff41f51100d9dd7a7e66312a64e0e542dba4b6b8..653af4625c63f0bc09500f9a1a31b85f3d6c2fba 100644
--- a/tests/float/oracle/special_floats.res.oracle
+++ b/tests/float/oracle/special_floats.res.oracle
@@ -1,16 +1,87 @@
-[kernel] Parsing tests/float/special_floats.i (no preprocessing)
+[kernel] Parsing tests/float/special_floats.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
rand ∈ [--..--]
+ any_double ∈ [--..--]
+ global_infinity ∈ {inf}
+ global_nan ∈ NaN
[eva] computing for function nan_comparisons <- main.
- Called from tests/float/special_floats.i:24.
+ Called from tests/float/special_floats.c:94.
[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.
+[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.
+[eva:alarm] tests/float/special_floats.c:31: Warning:
+ 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:
+ 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:
+ check 'false' got status invalid.
+[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:
+ 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:50: 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:
+ assertion got status unknown.
+[eva:alarm] tests/float/special_floats.c:55: Warning:
+ assertion got status unknown.
+[eva] tests/float/special_floats.c:56:
+ Frama_C_show_each_finite_nan:
+ [-1.79769313486e+308 .. 1.79769313486e+308] ∪ {NaN}
+[eva:alarm] tests/float/special_floats.c:59: Warning:
+ assertion got status unknown.
+[eva] tests/float/special_floats.c:60:
+ Frama_C_show_each_top: [-inf .. inf] ∪ {NaN}
+[eva:alarm] tests/float/special_floats.c:63: Warning:
+ assertion got status unknown.
+[eva] tests/float/special_floats.c:64: Frama_C_show_each_pos_infinity: {inf;NaN}
+[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.
+[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.
+[eva] Recording results for macro_nan
+[eva] Done for function macro_nan
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function is_infinite:
+ zero ∈ {-0.}
+ inf ∈ {inf}
+ nan_0 ∈ NaN
+ d ∈ [-inf .. inf] ∪ {NaN}
+[eva:final-states] Values at end of function macro_infinity:
+ infinity_f ∈ {inf}
+ infinity_d ∈ {inf}
+[eva:final-states] Values at end of function macro_nan:
+ nan_f ∈ NaN
[eva:final-states] Values at end of function nan_comparisons:
n ∈ NaN
d ∈ [-10. .. 10.]
diff --git a/tests/float/special_floats.c b/tests/float/special_floats.c
new file mode 100644
index 0000000000000000000000000000000000000000..1e07cd3a6ba385e0b3eec0bda2eb0aa1381200d3
--- /dev/null
+++ b/tests/float/special_floats.c
@@ -0,0 +1,98 @@
+/* run.config*
+ OPT: -eva @EVA_CONFIG@ -warn-special-float none
+*/
+
+/* Tests on special float values NaN and infinites. */
+
+volatile int rand;
+volatile double any_double;
+
+/* All comparisons involving NaN are false, except for inequalities that are
+ true. */
+void nan_comparisons () {
+ double n = 0.0 / 0.0;
+ double d = rand ? -10. : 10.;
+ int eq1 = (n == n) ? 1 : 0;
+ int comp1 = (n < n) ? 1 : 0;
+ int ne1 = (n != n) ? 1 : 0;
+ int eq2 = (n == d) ? 1 : 0;
+ int comp2 = (n < d) ? 1 : 0;
+ int ne2 = (n != d) ? 1 : 0;
+}
+
+#include <math.h>
+
+/* Tests the logical predicates \is_plus_infinite & co. */
+void is_infinite () {
+ /* Tests the evaluation on singletons. */
+ double zero = -0.;
+ /*@ check true: \is_finite(zero); */
+ /*@ check false: !\is_finite(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_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_plus_infinity(nan); */
+ /*@ check false: \is_minus_infinity(nan); */
+ double d = any_double;
+ /* Tests the reduction by assertions. */
+ if (rand) {
+ /*@ assert \is_plus_infinity(d); */
+ Frama_C_show_each_pos_infinity(d);
+ }
+ if (rand) {
+ /*@ assert \is_minus_infinity(d); */
+ Frama_C_show_each_neg_infinity(d);
+ }
+ if (rand) {
+ /*@ assert !\is_plus_infinity(d); */
+ /*@ assert !\is_minus_infinity(d); */
+ Frama_C_show_each_finite_nan(d);
+ }
+ if (rand) {
+ /*@ assert !\is_finite(d); */
+ Frama_C_show_each_top(d);
+ }
+ if (d > 0.) {
+ /*@ assert !\is_finite(d); */
+ Frama_C_show_each_pos_infinity(d);
+ }
+}
+
+float global_infinity = INFINITY;
+float global_nan = NAN;
+
+/* Tests the C and logic macros INFINITY and HUGE_VAL. */
+void macro_infinity () {
+ float infinity_f = INFINITY;
+ Frama_C_show_each_infinity(infinity_f);
+ /*@ assert \eq_float(infinity_f,INFINITY); @*/
+ double infinity_d = HUGE_VAL;
+ if(INFINITY != infinity_d)
+ /*@ assert \false; @*/;
+}
+
+/* Tests the C and logic macros NAN. */
+void macro_nan () {
+ float nan_f = NAN;
+ Frama_C_show_each_nan(nan_f);
+ /*@ assert \is_NaN(nan_f); @*/
+ /*@ assert \ne_float(nan_f,NAN); @*/
+ /*@ assert \subset({nan_f},{NAN}); @*/
+ if(NAN == nan_f)
+ /*@ assert \false; @*/;
+}
+
+
+void main () {
+ nan_comparisons ();
+ is_infinite ();
+ macro_infinity ();
+ macro_nan ();
+}
diff --git a/tests/float/special_floats.i b/tests/float/special_floats.i
deleted file mode 100644
index 191afecec7da2c637a90355d92a23dbab8bb23d0..0000000000000000000000000000000000000000
--- a/tests/float/special_floats.i
+++ /dev/null
@@ -1,25 +0,0 @@
-/* run.config*
- OPT: -eva @EVA_CONFIG@ -warn-special-float none
-*/
-
-/* Tests on special float values NaN and infinites. */
-
-volatile int rand;
-
-
-/* All comparisons involving NaN are false, except for inequalities that are
- true. */
-void nan_comparisons () {
- double n = 0.0 / 0.0;
- double d = rand ? -10. : 10.;
- int eq1 = (n == n) ? 1 : 0;
- int comp1 = (n < n) ? 1 : 0;
- int ne1 = (n != n) ? 1 : 0;
- int eq2 = (n == d) ? 1 : 0;
- int comp2 = (n < d) ? 1 : 0;
- int ne2 = (n != d) ? 1 : 0;
-}
-
-void main () {
- nan_comparisons ();
-}
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 0f3499f8f38e8e1815a6b7f9bb68d54d3019a961..ace1c0568b9fc422d31f7bfa9b341f94f18c509d 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -2161,7 +2161,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 71)
+[ Extern ] Froms (file share/libc/math.h, line 67)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2205,7 +2205,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 95)
+[ Extern ] Froms (file share/libc/math.h, line 91)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2237,28 +2237,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 132)
+[ Extern ] Assigns (file share/libc/math.h, line 128)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 139)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 135)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 132)
+[ Extern ] Froms (file share/libc/math.h, line 128)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 132)
+[ Extern ] Froms (file share/libc/math.h, line 128)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 139)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 135)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 139)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 135)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 135)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 131)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2281,28 +2281,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 146)
+[ Extern ] Assigns (file share/libc/math.h, line 142)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 153)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 149)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 146)
+[ Extern ] Froms (file share/libc/math.h, line 142)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 146)
+[ Extern ] Froms (file share/libc/math.h, line 142)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 153)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 149)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 153)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 149)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 149)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 145)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2325,28 +2325,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 160)
+[ Extern ] Assigns (file share/libc/math.h, line 156)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 167)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 163)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 160)
+[ Extern ] Froms (file share/libc/math.h, line 156)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 160)
+[ Extern ] Froms (file share/libc/math.h, line 156)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 167)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 163)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 167)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 163)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 163)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 159)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2369,28 +2369,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 174)
+[ Extern ] Assigns (file share/libc/math.h, line 170)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 181)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 177)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 174)
+[ Extern ] Froms (file share/libc/math.h, line 170)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 174)
+[ Extern ] Froms (file share/libc/math.h, line 170)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 181)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 177)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 181)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 177)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 177)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 173)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2413,28 +2413,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 188)
+[ Extern ] Assigns (file share/libc/math.h, line 184)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 195)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 191)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 188)
+[ Extern ] Froms (file share/libc/math.h, line 184)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 188)
+[ Extern ] Froms (file share/libc/math.h, line 184)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 195)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 191)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 195)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 191)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 191)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 187)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2457,28 +2457,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 202)
+[ Extern ] Assigns (file share/libc/math.h, line 198)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 209)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 205)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 202)
+[ Extern ] Froms (file share/libc/math.h, line 198)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 202)
+[ Extern ] Froms (file share/libc/math.h, line 198)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 209)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 205)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 209)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 205)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 205)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 201)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2504,7 +2504,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 216)
+[ Extern ] Froms (file share/libc/math.h, line 212)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2524,7 +2524,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 223)
+[ Extern ] Froms (file share/libc/math.h, line 219)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2544,7 +2544,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 230)
+[ Extern ] Froms (file share/libc/math.h, line 226)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2561,7 +2561,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 238)
+[ Extern ] Froms (file share/libc/math.h, line 234)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2578,7 +2578,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 245)
+[ Extern ] Froms (file share/libc/math.h, line 241)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2601,7 +2601,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 253)
+[ Extern ] Froms (file share/libc/math.h, line 249)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2621,7 +2621,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 260)
+[ Extern ] Froms (file share/libc/math.h, line 256)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2641,7 +2641,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 267)
+[ Extern ] Froms (file share/libc/math.h, line 263)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2661,7 +2661,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 274)
+[ Extern ] Froms (file share/libc/math.h, line 270)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2681,7 +2681,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 281)
+[ Extern ] Froms (file share/libc/math.h, line 277)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2701,7 +2701,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 288)
+[ Extern ] Froms (file share/libc/math.h, line 284)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2721,10 +2721,10 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 299)
+[ Extern ] Assigns (file share/libc/math.h, line 295)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 310)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 306)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'infinite' nothing
@@ -2733,22 +2733,22 @@
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 299)
+[ Extern ] Froms (file share/libc/math.h, line 295)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 299)
+[ Extern ] Froms (file share/libc/math.h, line 295)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 310)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 306)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 310)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 306)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 306)
+[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 302)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 302)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 298)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2777,10 +2777,10 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 317)
+[ Extern ] Assigns (file share/libc/math.h, line 313)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 328)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 324)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'infinite' nothing
@@ -2789,22 +2789,22 @@
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 317)
+[ Extern ] Froms (file share/libc/math.h, line 313)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 317)
+[ Extern ] Froms (file share/libc/math.h, line 313)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 328)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 324)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 328)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 324)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 324)
+[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 320)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 320)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 316)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2833,10 +2833,10 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 335)
+[ Extern ] Assigns (file share/libc/math.h, line 331)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 346)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 342)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'infinite' nothing
@@ -2845,22 +2845,22 @@
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 335)
+[ Extern ] Froms (file share/libc/math.h, line 331)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 335)
+[ Extern ] Froms (file share/libc/math.h, line 331)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 346)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 342)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 346)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 342)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 342)
+[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 338)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 338)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 334)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2889,7 +2889,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 374)
+[ Extern ] Froms (file share/libc/math.h, line 370)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2909,7 +2909,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 382)
+[ Extern ] Froms (file share/libc/math.h, line 378)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2926,7 +2926,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 412)
+[ Extern ] Froms (file share/libc/math.h, line 408)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2943,7 +2943,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 419)
+[ Extern ] Froms (file share/libc/math.h, line 415)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2960,7 +2960,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 426)
+[ Extern ] Froms (file share/libc/math.h, line 422)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2977,7 +2977,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 433)
+[ Extern ] Froms (file share/libc/math.h, line 429)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2994,7 +2994,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 440)
+[ Extern ] Froms (file share/libc/math.h, line 436)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3011,7 +3011,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 447)
+[ Extern ] Froms (file share/libc/math.h, line 443)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3028,7 +3028,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 458)
+[ Extern ] Froms (file share/libc/math.h, line 454)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3045,7 +3045,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 465)
+[ Extern ] Froms (file share/libc/math.h, line 461)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3062,7 +3062,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 472)
+[ Extern ] Froms (file share/libc/math.h, line 468)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3087,7 +3087,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 498)
+[ Extern ] Froms (file share/libc/math.h, line 494)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3112,7 +3112,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 506)
+[ Extern ] Froms (file share/libc/math.h, line 502)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3137,7 +3137,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 514)
+[ Extern ] Froms (file share/libc/math.h, line 510)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3154,7 +3154,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 527)
+[ Extern ] Froms (file share/libc/math.h, line 523)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3171,7 +3171,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 534)
+[ Extern ] Froms (file share/libc/math.h, line 530)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3197,7 +3197,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 543)
+[ Extern ] Froms (file share/libc/math.h, line 539)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3217,7 +3217,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 551)
+[ Extern ] Froms (file share/libc/math.h, line 547)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3237,7 +3237,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 559)
+[ Extern ] Froms (file share/libc/math.h, line 555)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3254,7 +3254,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 582)
+[ Extern ] Froms (file share/libc/math.h, line 578)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3271,7 +3271,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 588)
+[ Extern ] Froms (file share/libc/math.h, line 584)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3288,7 +3288,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 595)
+[ Extern ] Froms (file share/libc/math.h, line 591)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3305,7 +3305,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 601)
+[ Extern ] Froms (file share/libc/math.h, line 597)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3322,7 +3322,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 607)
+[ Extern ] Froms (file share/libc/math.h, line 603)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3339,7 +3339,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 613)
+[ Extern ] Froms (file share/libc/math.h, line 609)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3356,7 +3356,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 635)
+[ Extern ] Froms (file share/libc/math.h, line 631)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3373,7 +3373,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 641)
+[ Extern ] Froms (file share/libc/math.h, line 637)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3390,7 +3390,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 647)
+[ Extern ] Froms (file share/libc/math.h, line 643)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3407,7 +3407,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 661)
+[ Extern ] Froms (file share/libc/math.h, line 657)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3424,7 +3424,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 667)
+[ Extern ] Froms (file share/libc/math.h, line 663)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3441,7 +3441,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 673)
+[ Extern ] Froms (file share/libc/math.h, line 669)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3458,7 +3458,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 680)
+[ Extern ] Froms (file share/libc/math.h, line 676)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3475,7 +3475,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 687)
+[ Extern ] Froms (file share/libc/math.h, line 683)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3492,7 +3492,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 708)
+[ Extern ] Froms (file share/libc/math.h, line 704)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3509,7 +3509,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 715)
+[ Extern ] Froms (file share/libc/math.h, line 711)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3526,13 +3526,47 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 722)
+[ Extern ] Froms (file share/libc/math.h, line 718)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
+--------------------------------------------------------------------------------
+--- Properties of Function '__fc_infinity'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'result_is_infinity'
+ ensures result_is_infinity: \is_plus_infinity(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 766)
+ assigns \result \from \nothing;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function '__fc_nan'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'result_is_nan'
+ ensures result_is_nan: \is_NaN(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 772)
+ assigns \result \from \nothing;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+
--------------------------------------------------------------------------------
--- Properties of Function 'idct'
--------------------------------------------------------------------------------
@@ -3888,9 +3922,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 173 Completely validated
+ 175 Completely validated
16 Locally validated
- 448 Considered valid
+ 454 Considered valid
56 To be validated
- 693 Total
+ 701 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index d64ea807afda96b59b16bcca76633b124b9864dc..e8cb83c5ada4c1850d6cd7cd3708da2ec16145dc 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -40,7 +40,7 @@
unsetenv (0 call); wcscat (0 call); wcscpy (0 call); wcslen (2 calls);
wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call);
- Undefined functions (382)
+ Undefined functions (384)
=========================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -61,64 +61,64 @@
__builtin_umull_overflow (0 call); __builtin_umulll_overflow (0 call);
__builtin_usub_overflow (0 call); __builtin_usubl_overflow (0 call);
__builtin_usubll_overflow (0 call); __fc_fpclassify (0 call);
- __fc_fpclassifyf (0 call); __va_fcntl_flock (0 call);
- __va_fcntl_int (0 call); __va_fcntl_void (0 call); __va_ioctl_int (0 call);
- __va_ioctl_ptr (0 call); __va_ioctl_void (0 call);
- __va_open_mode_t (0 call); __va_open_void (0 call);
- __va_openat_mode_t (0 call); __va_openat_void (0 call); _exit (0 call);
- abort (0 call); accept (0 call); access (0 call); acos (0 call);
- acosf (0 call); acosh (0 call); acoshf (0 call); acoshl (0 call);
- acosl (0 call); alloca (0 call); asin (0 call); asinf (0 call);
- asinl (0 call); at_quick_exit (0 call); atan (0 call); atan2 (0 call);
- atan2f (0 call); atanf (0 call); atanl (0 call); atexit (0 call);
- atof (0 call); atol (0 call); atoll (0 call); basename (0 call);
- bind (0 call); bsearch (0 call); bzero (0 call); ceil (0 call);
- ceilf (0 call); ceill (0 call); chdir (0 call); chown (0 call);
- chroot (0 call); clearerr (0 call); clearerr_unlocked (0 call);
- clock (0 call); clock_gettime (0 call); clock_nanosleep (0 call);
- close (0 call); closedir (0 call); closelog (0 call); connect (0 call);
- cos (0 call); cosf (0 call); cosl (0 call); creat (0 call); ctime (0 call);
- difftime (0 call); dirname (0 call); div (0 call); drand48 (0 call);
- dup (0 call); dup2 (0 call); erand48 (0 call); execl (0 call);
- execle (0 call); execlp (0 call); execv (0 call); execve (0 call);
- execvp (0 call); exit (0 call); exp (0 call); expf (0 call); fabsl (0 call);
- fclose (0 call); fcntl (0 call); fdopen (0 call); feof (2 calls);
- feof_unlocked (0 call); ferror (2 calls); ferror_unlocked (0 call);
- fflush (0 call); fgetc (1 call); fgetpos (0 call); fgets (0 call);
- fgetws (0 call); fileno (0 call); fileno_unlocked (0 call); flock (0 call);
- flockfile (0 call); floor (0 call); floorf (0 call); floorl (0 call);
- fmod (0 call); fmodf (0 call); fopen (0 call); fork (0 call);
- fputc (0 call); fputs (0 call); fread (0 call); free (1 call);
- freeaddrinfo (0 call); freopen (0 call); fseek (0 call); fsetpos (0 call);
- ftell (0 call); ftrylockfile (0 call); funlockfile (0 call);
- fwrite (0 call); gai_strerror (0 call); getc (0 call);
- getc_unlocked (0 call); getchar (0 call); getchar_unlocked (0 call);
- getcwd (0 call); getegid (0 call); geteuid (0 call); getgid (0 call);
- gethostname (0 call); getitimer (0 call); getopt (0 call);
- getopt_long (0 call); getopt_long_only (0 call); getpgid (0 call);
- getpgrp (0 call); getpid (0 call); getppid (0 call); getpriority (0 call);
- getpwnam (0 call); getpwuid (0 call); getresgid (0 call);
- getresuid (0 call); getrlimit (0 call); getrusage (0 call); gets (0 call);
- getsid (0 call); getsockopt (0 call); gettimeofday (0 call);
- getuid (0 call); gmtime (0 call); htonl (0 call); htons (0 call);
- iconv (0 call); iconv_close (0 call); iconv_open (0 call);
- inet_addr (2 calls); inet_ntoa (0 call); inet_ntop (0 call);
- inet_pton (0 call); isascii (0 call); isatty (0 call); jrand48 (0 call);
- kill (0 call); killpg (0 call); labs (0 call); lcong48 (0 call);
- ldiv (0 call); listen (0 call); llabs (0 call); lldiv (0 call);
- localtime (0 call); log (0 call); log10 (0 call); log10f (0 call);
- log10l (0 call); log2 (0 call); log2f (0 call); log2l (0 call);
- logf (0 call); logl (0 call); longjmp (0 call); lrand48 (0 call);
- lseek (0 call); malloc (7 calls); mblen (0 call); mbstowcs (0 call);
- mbtowc (0 call); mkdir (0 call); mkstemp (0 call); mktime (0 call);
- mrand48 (0 call); nan (0 call); nanf (0 call); nanl (0 call);
- nanosleep (0 call); nrand48 (0 call); ntohl (0 call); ntohs (0 call);
- open (0 call); openat (0 call); opendir (0 call); openlog (0 call);
- pathconf (0 call); pclose (0 call); perror (0 call); pipe (0 call);
- poll (0 call); popen (0 call); pow (0 call); powf (0 call);
- pthread_cond_broadcast (0 call); pthread_cond_destroy (0 call);
- pthread_cond_init (0 call); pthread_cond_wait (0 call);
- pthread_create (0 call); pthread_join (0 call);
+ __fc_fpclassifyf (0 call); __fc_infinity (0 call); __fc_nan (0 call);
+ __va_fcntl_flock (0 call); __va_fcntl_int (0 call);
+ __va_fcntl_void (0 call); __va_ioctl_int (0 call); __va_ioctl_ptr (0 call);
+ __va_ioctl_void (0 call); __va_open_mode_t (0 call);
+ __va_open_void (0 call); __va_openat_mode_t (0 call);
+ __va_openat_void (0 call); _exit (0 call); abort (0 call); accept (0 call);
+ access (0 call); acos (0 call); acosf (0 call); acosh (0 call);
+ acoshf (0 call); acoshl (0 call); acosl (0 call); alloca (0 call);
+ asin (0 call); asinf (0 call); asinl (0 call); at_quick_exit (0 call);
+ atan (0 call); atan2 (0 call); atan2f (0 call); atanf (0 call);
+ atanl (0 call); atexit (0 call); atof (0 call); atol (0 call);
+ atoll (0 call); basename (0 call); bind (0 call); bsearch (0 call);
+ bzero (0 call); ceil (0 call); ceilf (0 call); ceill (0 call);
+ chdir (0 call); chown (0 call); chroot (0 call); clearerr (0 call);
+ clearerr_unlocked (0 call); clock (0 call); clock_gettime (0 call);
+ clock_nanosleep (0 call); close (0 call); closedir (0 call);
+ closelog (0 call); connect (0 call); cos (0 call); cosf (0 call);
+ cosl (0 call); creat (0 call); ctime (0 call); difftime (0 call);
+ dirname (0 call); div (0 call); drand48 (0 call); dup (0 call);
+ dup2 (0 call); erand48 (0 call); execl (0 call); execle (0 call);
+ execlp (0 call); execv (0 call); execve (0 call); execvp (0 call);
+ exit (0 call); exp (0 call); expf (0 call); fabsl (0 call); fclose (0 call);
+ fcntl (0 call); fdopen (0 call); feof (2 calls); feof_unlocked (0 call);
+ ferror (2 calls); ferror_unlocked (0 call); fflush (0 call); fgetc (1 call);
+ fgetpos (0 call); fgets (0 call); fgetws (0 call); fileno (0 call);
+ fileno_unlocked (0 call); flock (0 call); flockfile (0 call);
+ floor (0 call); floorf (0 call); floorl (0 call); fmod (0 call);
+ fmodf (0 call); fopen (0 call); fork (0 call); fputc (0 call);
+ fputs (0 call); fread (0 call); free (1 call); freeaddrinfo (0 call);
+ freopen (0 call); fseek (0 call); fsetpos (0 call); ftell (0 call);
+ ftrylockfile (0 call); funlockfile (0 call); fwrite (0 call);
+ gai_strerror (0 call); getc (0 call); getc_unlocked (0 call);
+ getchar (0 call); getchar_unlocked (0 call); getcwd (0 call);
+ getegid (0 call); geteuid (0 call); getgid (0 call); gethostname (0 call);
+ getitimer (0 call); getopt (0 call); getopt_long (0 call);
+ getopt_long_only (0 call); getpgid (0 call); getpgrp (0 call);
+ getpid (0 call); getppid (0 call); getpriority (0 call); getpwnam (0 call);
+ getpwuid (0 call); getresgid (0 call); getresuid (0 call);
+ getrlimit (0 call); getrusage (0 call); gets (0 call); getsid (0 call);
+ getsockopt (0 call); gettimeofday (0 call); getuid (0 call);
+ gmtime (0 call); htonl (0 call); htons (0 call); iconv (0 call);
+ iconv_close (0 call); iconv_open (0 call); inet_addr (2 calls);
+ inet_ntoa (0 call); inet_ntop (0 call); inet_pton (0 call);
+ isascii (0 call); isatty (0 call); jrand48 (0 call); kill (0 call);
+ killpg (0 call); labs (0 call); lcong48 (0 call); ldiv (0 call);
+ listen (0 call); llabs (0 call); lldiv (0 call); localtime (0 call);
+ log (0 call); log10 (0 call); log10f (0 call); log10l (0 call);
+ log2 (0 call); log2f (0 call); log2l (0 call); logf (0 call); logl (0 call);
+ longjmp (0 call); lrand48 (0 call); lseek (0 call); malloc (7 calls);
+ mblen (0 call); mbstowcs (0 call); mbtowc (0 call); mkdir (0 call);
+ mkstemp (0 call); mktime (0 call); mrand48 (0 call); nan (0 call);
+ nanf (0 call); nanl (0 call); nanosleep (0 call); nrand48 (0 call);
+ ntohl (0 call); ntohs (0 call); open (0 call); openat (0 call);
+ opendir (0 call); openlog (0 call); pathconf (0 call); pclose (0 call);
+ perror (0 call); pipe (0 call); poll (0 call); popen (0 call); pow (0 call);
+ powf (0 call); pthread_cond_broadcast (0 call);
+ pthread_cond_destroy (0 call); pthread_cond_init (0 call);
+ pthread_cond_wait (0 call); pthread_create (0 call); pthread_join (0 call);
pthread_mutex_destroy (0 call); pthread_mutex_init (0 call);
pthread_mutex_lock (0 call); pthread_mutex_unlock (0 call); putc (0 call);
putc_unlocked (0 call); putchar (0 call); putchar_unlocked (0 call);
@@ -178,7 +178,7 @@
Goto = 89
Assignment = 438
Exit point = 82
- Function = 464
+ Function = 466
Function call = 89
Pointer dereferencing = 158
Cyclomatic complexity = 286
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index f1bb1d42421189f8e087c94215e6f4d70d1cf335..b85450e07ee183420637f89e3cd128f4c31ce19d 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3385,6 +3385,23 @@ int __finitef(float f);
int __finite(double d);
+/*@ logic float __fc_infinity(ℤ x) = \plus_infinity;
+ */
+/*@ logic float __fc_nan(ℤ x) = \NaN;
+
+*/
+/*@ ensures result_is_infinity: \is_plus_infinity(\result);
+ assigns \result;
+ assigns \result \from \nothing;
+ */
+extern float __fc_infinity(int x);
+
+/*@ ensures result_is_nan: \is_NaN(\result);
+ assigns \result;
+ assigns \result \from \nothing;
+ */
+extern float __fc_nan(int x);
+
/*@ requires finite_arg: \is_finite(x);
ensures res_finite: \is_finite(\result);
ensures positive_result: \result ≥ 0.;