Merge pull request #5754 from tautschnig/fix-5542

Support c_bool in expr2bits/bits2expr

Author: kroening

regression/cbmc/Bool5/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <string.h>
+
+struct conft
+{
+  _Bool red;
+  int one;
+};
+
+int main()
+{
+  struct conft conf_init = {0, 1};
+  struct conft my_conf;
+  memcpy((char *)&my_conf, (char *)&conf_init, sizeof(struct conft));
+  int num = my_conf.one;
+  assert(num == 1);
+  return 0;
+}

regression/cbmc/Bool5/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+Generated 4 VCC\(s\), 0 remaining after simplification
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/util/simplify_utils.cpp

@@ -191,7 +191,7 @@ optionalt<exprt> bits2expr(
     type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
     type.id() == ID_floatbv || type.id() == ID_fixedbv ||
     type.id() == ID_c_bit_field || type.id() == ID_pointer ||
-    type.id() == ID_bv)
+    type.id() == ID_bv || type.id() == ID_c_bool)
   {
     endianness_mapt map(type, little_endian, ns);
 
@@ -385,7 +385,8 @@ expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
     if(
       type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
       type.id() == ID_floatbv || type.id() == ID_fixedbv ||
-      type.id() == ID_c_bit_field || type.id() == ID_bv)
+      type.id() == ID_c_bit_field || type.id() == ID_bv ||
+      type.id() == ID_c_bool)
     {
       const auto width = to_bitvector_type(type).get_width();