Skip to content
Snippets Groups Projects
Commit 0ad33a7c authored by David Bühler's avatar David Bühler Committed by Andre Maroneze
Browse files

[Libc] Fixes the declaration of __fc_nan and names ensures clauses.

parent ddaf0c19
No related branches found
No related tags found
No related merge requests found
......@@ -762,16 +762,16 @@ extern int __finite(double d);
@*/
/*@
ensures \eq_float(\result,\plus_infinity);
ensures result_is_infinity: \is_plus_infinity(\result);
assigns \result \from \nothing;
@*/
extern const float __fc_infinity(int x);
/*@
ensures \is_NaN(\result);
ensures result_is_nan: \is_NaN(\result);
assigns \result \from \nothing;
@*/
extern const float __fc_nan();
extern const float __fc_nan(int x);
#define INFINITY __fc_infinity(0)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment