C library: do not flag division-by-zero when building NaN

We construct NaN (and Inf) by dividing by zero, which is a
standards-compliant way in that Nan (Inf) is the correct result for
these cases. Do not flag these operations as division-by-zero, which the
user would not expect.

Author: tautschnig

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

@@ -1,9 +1,19 @@
 #include <assert.h>
+#include <float.h>
 #include <math.h>
 
 int main()
 {
   double four = pow(2.0, 2.0);
   assert(four > 3.999 && four < 4.345);
+
+  double x;
+  __CPROVER_assume(isnormal(x));
+  double limit = 1 << 15;
+  __CPROVER_assume(x > -limit && x < limit);
+  __CPROVER_assume(x > FLT_MIN || x < -FLT_MIN);
+  double sq = pow(x, 2.0);
+  assert(sq >= 0.0);
+
   return 0;
 }