division-by-zero on float

This disables the division-by-zero check for floating-point operations.
Division by zero on floating-point numbers is defined behavior when using
IEEE 754.

Author: kroening

regression/cbmc/pragma_cprover_enable_all/main.c

@@ -30,9 +30,9 @@ int main()
     char *p = malloc(N * sizeof(*p));
     char *q;
     char *r;
-    float den;
-    float x;
-    float y;
+    int den;
+    int x;
+    int y;
     ABC e;
     bool readable;
     char i;
@@ -41,9 +41,9 @@ int main()
     q = p + 2000000000000;
     q = r;
     if(nondet_bool())
-      den = 0.0;
+      den = 0;
     else
-      den = 1.0;
+      den = 1;
     y = x / den;
     e = 10;
     i += 1;
@@ -67,9 +67,9 @@ int main()
     char *p = malloc(N * sizeof(*p));
     char *q;
     char *r;
-    float den;
-    float x;
-    float y;
+    int den;
+    int x;
+    int y;
     ABC e;
     bool readable;
     char i;
@@ -78,9 +78,9 @@ int main()
     q = p + 2000000000000;
     q = r;
     if(nondet_bool())
-      den = 0.0;
+      den = 0;
     else
-      den = 1.0;
+      den = 1;
     y = x / den;
     e = 10;
     i += 1;

regression/cbmc/pragma_cprover_enable_all/test.desc

@@ -4,9 +4,8 @@ main.c
 ^\[main\.pointer_primitives\.\d+\] line 77 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
 ^\[main\.pointer_primitives\.\d+\] line 77 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
 ^\[main\.pointer_arithmetic\.\d+\] line 78 pointer arithmetic: pointer outside object bounds in p \+ (\(signed int\))?2000000000000(l|ll): FAILURE
-^\[main\.NaN\.\d+\] line 84 NaN on / in x / den: FAILURE
 ^\[main\.division-by-zero\.\d+\] line 84 division by zero in x / den: FAILURE
-^\[main\.overflow\.\d+\] line 84 arithmetic overflow on floating-point division in x / den: FAILURE
+^\[main\.overflow\.\d+\] line 84 arithmetic overflow on signed division in x / den: SUCCESS
 ^\[main\.enum-range-check\.\d+\] line 85 enum range check in \(ABC\)10: FAILURE
 ^\[main\.overflow\.\d+\] line 86 arithmetic overflow on signed (to unsigned )?type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE
 ^\[main\.overflow\.\d+\] line 87 arithmetic overflow on signed \+ in j \+ 1: FAILURE
@@ -17,9 +16,8 @@ main.c
 ^\[main\.pointer_primitives\.\d+\] line 40 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
 ^\[main\.pointer_primitives\.\d+\] line 40 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
 ^\[main\.pointer_arithmetic\.\d+\] line 41 pointer arithmetic: pointer outside object bounds in p \+ .*2000000000000(l|ll): FAILURE
-^\[main\.NaN\.\d+\] line 47 NaN on / in x / den: FAILURE
 ^\[main\.division-by-zero\.\d+\] line 47 division by zero in x / den: FAILURE
-^\[main\.overflow\.\d+\] line 47 arithmetic overflow on floating-point division in x / den: FAILURE
+^\[main\.overflow\.\d+\] line 47 arithmetic overflow on signed division in x / den: SUCCESS
 ^\[main\.enum-range-check\.\d+\] line 48 enum range check in \(ABC\)10: FAILURE
 ^\[main\.overflow\.\d+\] line 49 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\): FAILURE
 ^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed \+ in j \+ 1: FAILURE

src/ansi-c/goto_check_c.cpp

@@ -1850,7 +1850,15 @@ void goto_check_ct::check_rec_div(
   const div_exprt &div_expr,
   const guardt &guard)
 {
-  div_by_zero_check(to_div_expr(div_expr), guard);
+  if(
+    div_expr.type().id() == ID_signedbv ||
+    div_expr.type().id() == ID_unsignedbv || div_expr.type().id() == ID_c_bool)
+  {
+    // Division by zero is undefined behavior for all integer types.
+    // Division by zero is defined behavior for
+    // floating-point types if IEEE 754 is used.
+    div_by_zero_check(to_div_expr(div_expr), guard);
+  }
 
   if(div_expr.type().id() == ID_signedbv)
     integer_overflow_check(div_expr, guard);