Merge pull request #357 from peterschrammel/fix-c-bool-xml-output

Fix _Bool XML output

Author: Daniel Kroening

regression/cbmc/c99_Bool/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+void foo(_Bool y)
+{
+  int x;
+  if(y) 
+  {  
+    x=(int)y;
+    assert(x==1);
+  }
+}

regression/cbmc/c99_Bool/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--function foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/ansi_c_entry_point.cpp

@@ -73,6 +73,18 @@ exprt::operandst build_function_environment(
 
     init_code.add(decl);
 
+    // nondet init for _Bool
+    if(decl.symbol().type().id()==ID_c_bool)
+    {
+      code_assignt assign(
+        decl.symbol(),
+        typecast_exprt(
+          side_effect_expr_nondett(bool_typet()),
+          decl.symbol().type()));
+
+      init_code.move_to_operands(assign);
+    }
+
     codet input(ID_input);
     input.operands().resize(2);
 

src/util/json_expr.cpp

@@ -265,6 +265,15 @@ json_objectt json(
       result["binary"]=json_stringt(expr.is_true()?"1":"0");
       result["data"]=jsont::json_boolean(expr.is_true());
     }
+    else if(type.id()==ID_c_bool)
+    {
+      result["name"]=json_stringt("integer");
+      result["c_type"]=json_stringt("_Bool");
+      result["binary"]=json_stringt(expr.get_string(ID_value));
+      mp_integer b;
+      to_integer(to_constant_expr(expr), b);
+      result["data"]=json_stringt(integer2string(b));
+    }
     else
     {
       result["name"]=json_stringt("unknown");

src/util/xml_expr.cpp

@@ -126,7 +126,8 @@ xmlt xml(
   {
     result.name="vector";
     result.new_element("subtype").new_element()=xml(type.subtype(), ns);
-    result.new_element("size").new_element()=xml(to_vector_type(type).size(), ns);
+    result.new_element("size").new_element()=
+      xml(to_vector_type(type).size(), ns);
   }
   else if(type.id()==ID_struct)
   {
@@ -263,6 +264,15 @@ xmlt xml(
       result.set_attribute("binary", expr.is_true()?"1":"0");
       result.data=expr.is_true()?"TRUE":"FALSE";
     }
+    else if(type.id()==ID_c_bool)
+    {
+      result.name="integer";
+      result.set_attribute("c_type", "_Bool");
+      result.set_attribute("binary", expr.get_string(ID_value));
+      mp_integer b;
+      to_integer(to_constant_expr(expr), b);
+      result.data=integer2string(b);
+    }
     else
     {
       result.name="unknown";
@@ -309,7 +319,8 @@ xmlt xml(
 
     xmlt &e=result.new_element("member");
     e.new_element(xml(expr.op0(), ns));
-    e.set_attribute("member_name",
+    e.set_attribute(
+      "member_name",
       id2string(to_union_expr(expr).get_component_name()));
   }
   else