Merge pull request #5758 from tautschnig/bool

Handle bool expressions in implicit_typecast_arithmetic

Author: tautschnig

regression/ansi-c/int128_and_bool1/main.c

@@ -0,0 +1,6 @@
+int main(int argc, char *argv[])
+{
+  unsigned __int128 z;
+  z = (unsigned __int128)argc;
+  z += (argc < 1);
+}

regression/ansi-c/int128_and_bool1/test.desc

@@ -0,0 +1,7 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^CONVERSION ERROR$

regression/cbmc/enum9/main.c

@@ -0,0 +1,25 @@
+#include <limits.h>
+
+enum E
+{
+  V1 = 1,
+  V2 = 2
+};
+
+struct B
+{
+  unsigned b : 2;
+};
+
+int main()
+{
+  unsigned __int128 int x;
+  __CPROVER_assume(x < (~(unsigned __int128)0) - 4);
+
+  enum E e;
+  __CPROVER_assume(__CPROVER_enum_is_in_range(e));
+  __CPROVER_assert(x + e > x, "long long plus enum");
+
+  struct B b;
+  __CPROVER_assert(x + b.b >= x, "long long plus bitfield");
+}

regression/cbmc/enum9/test.desc

@@ -0,0 +1,9 @@
+CORE gcc-only
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^CONVERSION ERROR$
+^warning: ignoring

src/ansi-c/c_typecast.cpp

@@ -650,24 +650,8 @@ void c_typecastt::implicit_typecast_arithmetic(
 
   if(max_type==LARGE_SIGNED_INT || max_type==LARGE_UNSIGNED_INT)
   {
-    // get the biggest width of both
-    std::size_t width1 = to_bitvector_type(type1).get_width();
-    std::size_t width2 = to_bitvector_type(type2).get_width();
-
     // produce type
-    typet result_type;
-
-    if(width1==width2)
-    {
-      if(max_type==LARGE_SIGNED_INT)
-        result_type=signedbv_typet(width1);
-      else
-        result_type=unsignedbv_typet(width1);
-    }
-    else if(width1>width2)
-      result_type=type1;
-    else // width1<width2
-      result_type=type2;
+    typet result_type = (max_type == c_type1) ? type1 : type2;
 
     do_typecast(expr1, result_type);
     do_typecast(expr2, result_type);