C library: whitespace fix to make fmaxf, fmaxl available

We parse the comments for "FUNCTION:" and therefore must not have a
space before the colon.

Enable and add regression tests for all variants of fmax (and also its
dual fmin, while at it).

Author: tautschnig

regression/cbmc-library/fmax-01/main.c

@@ -3,7 +3,11 @@
 
 int main()
 {
-  fmax();
-  assert(0);
+  double d1, d2;
+  __CPROVER_assume(!isnan(d1) || !isnan(d2));
+  double r = fmax(d1, d2);
+  assert(!isnan(d1) || r == d2);
+  assert(!isnan(d2) || r == d1);
+  assert(isnan(d1) || isnan(d2) || (d1 > d2 ? r == d1 : r == d2));
   return 0;
 }

regression/cbmc-library/fmax-01/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --nan-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-library/fmaxf-01/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  float f1, f2;
+  __CPROVER_assume(!isnan(f1) || !isnan(f2));
+  float r = fmaxf(f1, f2);
+  assert(!isnan(f1) || r == f2);
+  assert(!isnan(f2) || r == f1);
+  assert(isnan(f1) || isnan(f2) || (f1 > f2 ? r == f1 : r == f2));
+  return 0;
+}

regression/cbmc-library/fmaxf-01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check --nan-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-library/fmaxl-01/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  long double d1, d2;
+  __CPROVER_assume(!isnan(d1) || !isnan(d2));
+  long double r = fmaxl(d1, d2);
+  assert(!isnan(d1) || r == d2);
+  assert(!isnan(d2) || r == d1);
+  assert(isnan(d1) || isnan(d2) || (d1 > d2 ? r == d1 : r == d2));
+  return 0;
+}

regression/cbmc-library/fmaxl-01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check --nan-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-library/fmin-01/main.c

@@ -3,7 +3,11 @@
 
 int main()
 {
-  fmin();
-  assert(0);
+  double d1, d2;
+  __CPROVER_assume(!isnan(d1) || !isnan(d2));
+  double r = fmin(d1, d2);
+  assert(!isnan(d1) || r == d2);
+  assert(!isnan(d2) || r == d1);
+  assert(isnan(d1) || isnan(d2) || (d1 < d2 ? r == d1 : r == d2));
   return 0;
 }

regression/cbmc-library/fmin-01/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --nan-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-library/fminf-01/main.c

@@ -3,7 +3,11 @@
 
 int main()
 {
-  fminf();
-  assert(0);
+  float f1, f2;
+  __CPROVER_assume(!isnan(f1) || !isnan(f2));
+  float r = fminf(f1, f2);
+  assert(!isnan(f1) || r == f2);
+  assert(!isnan(f2) || r == f1);
+  assert(isnan(f1) || isnan(f2) || (f1 < f2 ? r == f1 : r == f2));
   return 0;
 }

regression/cbmc-library/fminf-01/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --nan-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-library/fminl-01/main.c

@@ -3,7 +3,11 @@
 
 int main()
 {
-  fminl();
-  assert(0);
+  long double d1, d2;
+  __CPROVER_assume(!isnan(d1) || !isnan(d2));
+  long double r = fminl(d1, d2);
+  assert(!isnan(d1) || r == d2);
+  assert(!isnan(d2) || r == d1);
+  assert(isnan(d1) || isnan(d2) || (d1 < d2 ? r == d1 : r == d2));
   return 0;
 }

regression/cbmc-library/fminl-01/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --nan-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

src/ansi-c/library/math.c

@@ -955,7 +955,7 @@ long double sqrtl(long double d)
 // TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB
 double fmax(double f, double g) { return ((f >= g) || isnan(g)) ? f : g; }
 
-/* FUNCTION : fmaxf */
+/* FUNCTION: fmaxf */
 
 #ifndef __CPROVER_MATH_H_INCLUDED
 #include <math.h>
@@ -965,8 +965,7 @@ double fmax(double f, double g) { return ((f >= g) || isnan(g)) ? f : g; }
 // TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB
 float fmaxf(float f, float g) { return ((f >= g) || isnan(g)) ? f : g; }
 
-
-/* FUNCTION : fmaxl */
+/* FUNCTION: fmaxl */
 
 #ifndef __CPROVER_MATH_H_INCLUDED
 #include <math.h>