fix adjust_float_expressions

adjust_float_expressions adds a rounding mode to floating-point operations
when needed.  The fix does the following:

1) casts from/to c_bit_field DO need a rounding mode

2) casts from c_bool and bool DO NOT need a rounding mode

Author: Daniel Kroening

regression/cbmc/Float-no-simp1/main.c

@@ -1,10 +1,31 @@
+#include <assert.h>
+
+struct S
+{
+  unsigned int some_bit : 7;
+};
+
 int main()
 {
   unsigned int i, j;
   double d;
 
+  // double to integer and back
   i=100.0;
   d=i;
   j=d;
   assert(j==100);
+
+  // double to bool and back
+  _Bool b;
+  b = 100.0;
+  d = b;
+  assert(d);
+
+  // double to bit-field and back
+  struct S s;
+  s.some_bit = 100.0;
+  d = s.some_bit;
+  s.some_bit = d;
+  assert(s.some_bit == 100);
 }

src/goto-programs/adjust_float_expressions.cpp

@@ -53,16 +53,15 @@ static bool have_to_adjust_float_expressions(const exprt &expr)
     if(dest_type.id()==ID_floatbv &&
        src_type.id()==ID_floatbv)
       return true;
-    else if(dest_type.id()==ID_floatbv &&
-            (src_type.id()==ID_c_bool ||
-             src_type.id()==ID_signedbv ||
-             src_type.id()==ID_unsignedbv ||
-             src_type.id()==ID_c_enum_tag))
+    else if(
+      dest_type.id() == ID_floatbv &&
+      (src_type.id() == ID_c_bit_field || src_type.id() == ID_signedbv ||
+       src_type.id() == ID_unsignedbv || src_type.id() == ID_c_enum_tag))
       return true;
-    else if((dest_type.id()==ID_signedbv ||
-             dest_type.id()==ID_unsignedbv ||
-             dest_type.id()==ID_c_enum_tag) &&
-             src_type.id()==ID_floatbv)
+    else if(
+      (dest_type.id() == ID_signedbv || dest_type.id() == ID_unsignedbv ||
+       dest_type.id() == ID_c_enum_tag || dest_type.id() == ID_c_bit_field) &&
+      src_type.id() == ID_floatbv)
       return true;
   }
 
@@ -136,21 +135,26 @@ void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
       expr.operands().resize(2);
       expr.op1()=rounding_mode;
     }
-    else if(dest_type.id()==ID_floatbv &&
-            (src_type.id()==ID_c_bool ||
-             src_type.id()==ID_signedbv ||
-             src_type.id()==ID_unsignedbv ||
-             src_type.id()==ID_c_enum_tag))
+    else if(
+      dest_type.id() == ID_floatbv &&
+      (src_type.id() == ID_signedbv || src_type.id() == ID_unsignedbv ||
+       src_type.id() == ID_c_enum_tag || src_type.id() == ID_c_bit_field))
     {
       // casts from integer to float-type might round
       expr.id(ID_floatbv_typecast);
       expr.operands().resize(2);
       expr.op1()=rounding_mode;
     }
-    else if((dest_type.id()==ID_signedbv ||
-             dest_type.id()==ID_unsignedbv ||
-             dest_type.id()==ID_c_enum_tag) &&
-             src_type.id()==ID_floatbv)
+    else if(
+      dest_type.id() == ID_floatbv &&
+      (src_type.id() == ID_c_bool || src_type.id() == ID_bool))
+    {
+      // casts from bool or c_bool to float-type do not need rounding
+    }
+    else if(
+      (dest_type.id() == ID_signedbv || dest_type.id() == ID_unsignedbv ||
+       dest_type.id() == ID_c_enum_tag || dest_type.id() == ID_c_bit_field) &&
+      src_type.id() == ID_floatbv)
     {
       // In C, casts from float to integer always round to zero,
       // irrespectively of the rounding mode that is currently set.