Skip to content

Fix _Bool XML output #357

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
Jan 16, 2017
+53 −2
Merged

Fix _Bool XML output #357

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
298dbfb
Fix _Bool XML output
peterschrammel Dec 16, 2016
a174145
Fixed cpplint warnings
peterschrammel Dec 16, 2016
70b89c3
Ensure that _Bool parameter has only 0 or 1 values
peterschrammel Jan 7, 2017
2461ecf
Regression test for _Bool parameter
peterschrammel Jan 7, 2017
aaa5348
Fix _Bool JSON output
peterschrammel Jan 7, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions regression/cbmc/c99_Bool/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
#include <assert.h>

void foo(_Bool y)
{
int x;
if(y)
{
x=(int)y;
assert(x==1);
}
}
8 changes: 8 additions & 0 deletions regression/cbmc/c99_Bool/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
main.c
--function foo
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
12 changes: 12 additions & 0 deletions src/ansi-c/ansi_c_entry_point.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,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);

Expand Down
9 changes: 9 additions & 0 deletions src/util/json_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -266,6 +266,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");
Expand Down
15 changes: 13 additions & 2 deletions src/util/xml_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
{
Expand Down Expand Up @@ -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");
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is very confusing that an integer can be "FALSE" or "TRUE". Either there has to be a different result.name, or the value has to be 0/1.

Copy link
Member Author

@peterschrammel peterschrammel Dec 16, 2016 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Currently, we have non-1 solutions for "true" in the counterexample, which comes from the fact that we are looking for a non-0 solution when translating the conditional:
// 26 file cover_line_input_boolean.c line 4 function foo
IF !(par != FALSE && a == 1) THEN GOTO 1

However, C99, at least, demands that the values of _Bool are 0 and 1 only. We can output the actual integer value provided that we force "true" to be 1 elsewhere...

This is failing:

void main()
{
  int x;
  _Bool y;
  if(y) 
  {  
    x=(int)y;
    assert(x==1);
  }
}

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note that the above has undefined behaviour, i.e., it's good that this fails!
If you do y=nondet_bool(), with _Bool nondet_bool(), you get the expected result.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We have to explicitly initialise all parameters passed to the entry function otherwise the following would still fail:

void foo(_Bool y)
{
  int x;
  if(y) 
  {  
    x=(int)y;
    assert(x==1);
  }
}

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";
Expand Down Expand Up @@ -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
Expand Down