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

@@ -54,14 +54,15 @@ static bool have_to_adjust_float_expressions(const exprt &expr)
        src_type.id()==ID_floatbv)
       return true;
     else if(dest_type.id()==ID_floatbv &&
-            (src_type.id()==ID_c_bool ||
+            (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) &&
+             dest_type.id()==ID_c_enum_tag ||
+             dest_type.id()==ID_c_bit_field) &&
              src_type.id()==ID_floatbv)
       return true;
   }
@@ -137,19 +138,26 @@ void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
       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_signedbv ||
              src_type.id()==ID_unsignedbv ||
-             src_type.id()==ID_c_enum_tag))
+             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_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_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,