Add FMA special-case tests: NaN, infinity, 0*inf

Test IEEE 754 FMA special cases that were previously handled by
the C library model but are now handled by float_utilst::fma:
- fma(NaN, y, z) = NaN
- fma(x, NaN, z) = NaN
- fma(x, y, NaN) = NaN
- fma(0, inf, z) = NaN (0 * inf undefined)
- fma(inf, 0, z) = NaN
- fma(inf, x, -inf) = NaN (inf + (-inf) undefined)
- fma(inf, x, z) = +inf for finite z
- fma(x, y, inf) = +inf for finite x*y

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

regression/cbmc-library/fma/special_cases.c

@@ -0,0 +1,32 @@
+// IEEE 754 FMA special cases
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  // fma(NaN, y, z) = NaN
+  assert(isnan(fmaf(NAN, 1.0f, 0.0f)));
+
+  // fma(x, NaN, z) = NaN
+  assert(isnan(fmaf(1.0f, NAN, 0.0f)));
+
+  // fma(x, y, NaN) = NaN
+  assert(isnan(fmaf(1.0f, 1.0f, NAN)));
+
+  // fma(0, inf, z) = NaN (0 * inf is undefined)
+  assert(isnan(fmaf(0.0f, INFINITY, 1.0f)));
+
+  // fma(inf, 0, z) = NaN
+  assert(isnan(fmaf(INFINITY, 0.0f, 1.0f)));
+
+  // fma(inf, x, -inf) = NaN when inf*x = +inf (inf + (-inf) is undefined)
+  assert(isnan(fmaf(INFINITY, 1.0f, -INFINITY)));
+
+  // fma(inf, x, z) = +inf for finite z
+  assert(isinf(fmaf(INFINITY, 2.0f, 3.0f)));
+
+  // fma(x, y, inf) = +inf for finite x*y
+  assert(isinf(fmaf(2.0f, 3.0f, INFINITY)));
+
+  return 0;
+}

regression/cbmc-library/fma/test_special_cases.desc

@@ -0,0 +1,10 @@
+CORE
+special_cases.c
+--floatbv --no-built-in-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+IEEE 754 FMA special cases: NaN propagation, 0*inf, inf+(-inf), inf results.