Fix _Bool XML output #357
Fix _Bool XML output #357
Conversation
| e.set_attribute("member_name", | ||
| id2string(to_union_expr(expr).get_component_name())); | ||
| e.set_attribute( | ||
| "member_name", id2string(to_union_expr(expr).get_component_name())); |
There was a problem hiding this comment.
I would have put the id2string(...) on a new line.
peterschrammel
force-pushed
the
fix-c-bool-xml-output
branch
from
9e6fb6c to
a815869
Compare
| else if(type.id()==ID_c_bool) | ||
| { | ||
| result.name="integer"; | ||
| result.set_attribute("c_type", "_Bool"); |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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);
}
}
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.name="integer"; | ||
| result.set_attribute("c_type", "_Bool"); | ||
| result.set_attribute("binary", expr.get_string(ID_value)); | ||
| mp_integer bool_constant; |
There was a problem hiding this comment.
The "binary" should be 0/1; the above yields true/false.
There was a problem hiding this comment.
The binary is at least a byte...
There was a problem hiding this comment.
Indeed; will merge once value inconsistency is fixed.
peterschrammel
force-pushed
the
fix-c-bool-xml-output
branch
2 times, most recently
from
fae71be to
ace620d
Compare
|
@kroening, @tautschnig, updated. |
| mp_integer b; | ||
| to_integer(to_constant_expr(expr), b); | ||
| assert(b==mp_integer(0) || b==mp_integer(1)); | ||
| result["data"]=json_stringt(integer2string(b)); |
There was a problem hiding this comment.
The assertion is not guaranteed to hold; e.g., you can wreck this with a union, an uninitialised _Bool, or with a pointer typecast.
| typecast_exprt( | ||
| side_effect_expr_nondett(unsignedbv_typet(bool_width)), | ||
| decl.symbol().type())); | ||
|
|
There was a problem hiding this comment.
Use side_effect_expr_nondett(bool_typet()) instead.
peterschrammel
force-pushed
the
fix-c-bool-xml-output
branch
from
d0cdfbd to
aaa5348
Compare
…_traiting_of_models_lib_and_standard_lib Python driver improved traiting of models lib and Java standard lib
No description provided.