+double remainder (double x, double y) /*@*/ ;
+double remquo (double x, double y, /*@out@*/ int *quo) /*@modifies *quo@*/ ;
+double copysign (double x, double y) /*@*/ ;
+double nan (/*@nullterminated@*/ const char *tagp) /*@*/ ;
+double nextafter (double x, double y) /*@*/ ;
+double nextafterx (double x, long double y) /*@*/ ;
+
+double fdim (double x, double y) /*@modifies errno@*/ ;
+double fmax (double x, double y) /*@*/ ;
+double fmin (double x, double y) /*@*/ ;
+double fma (double x, double y, double z) /*@*/ ;
+
+int isgreater (s_real_t x, s_real_t y) /*@*/ ;
+int isgreaterequal (s_real_t x, s_real_t y) /*@*/ ;
+int isless (s_real_t x, s_real_t y) /*@*/ ;
+int islessequal (s_real_t x, s_real_t y) /*@*/ ;
+int islessgreater (s_real_t x, s_real_t y) /*@*/ ;
+int isunordered (s_real_t x, s_real_t y) /*@*/ ;