dump-c: fix output of _Bool-typed constants

Only __CPROVER_bool-typed constants can be used with exprt::is_true.
exprt::is_one's documentation promised that ID_c_bool was supported,
which wasn't actually the case. This commit fixes this and makes use of
is_one to fix the bug in dump-c.

Author: tautschnig

regression/goto-instrument/dump-bool/main.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main()
+{
+  _Bool v;
+  v = 1;
+  assert(v == 1);
+}

regression/goto-instrument/dump-bool/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--dump-c
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+irep
+--
+Dump-c previously always generated 0 for _Bool or __CPROVER_bool-typed
+constants. This test ensures that the value "1" is correctly generated.

src/goto-instrument/goto_program2code.cpp

@@ -1893,14 +1893,20 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
     }
     else if(expr.type().id()==ID_pointer)
       add_local_types(expr.type());
-    else if(expr.type().id()==ID_bool ||
-            expr.type().id()==ID_c_bool)
+    else if(expr.type().id() == ID_bool)
     {
       expr = typecast_exprt(
         from_integer(
           expr.is_true() ? 1 : 0, signedbv_typet(config.ansi_c.int_width)),
         bool_typet());
     }
+    else if(expr.type().id() == ID_c_bool)
+    {
+      expr = typecast_exprt(
+        from_integer(
+          expr.is_one() ? 1 : 0, signedbv_typet(config.ansi_c.int_width)),
+        c_bool_type());
+    }
 
     const irept &c_sizeof_type=expr.find(ID_C_c_sizeof_type);
 

src/util/expr.cpp

@@ -146,7 +146,9 @@ bool exprt::is_one() const
         CHECK_RETURN(false);
       return rat_value.is_one();
     }
-    else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
+    else if(
+      type_id == ID_unsignedbv || type_id == ID_signedbv ||
+      type_id == ID_c_bool || type_id == ID_c_bit_field)
     {
       const auto width = to_bitvector_type(type()).get_width();
       mp_integer int_value =