dump-c: fix output of _Bool-typed constants #5867
Conversation
tautschnig
requested review from
chrisr-diffblue,
hannes-steffenhagen-diffblue,
kroening,
martin-cs,
peterschrammel and
smowton
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #5867 +/- ##
===========================================
- Coverage 72.90% 72.90% -0.01%
===========================================
Files 1423 1425 +2
Lines 154159 154282 +123
===========================================
+ Hits 112397 112485 +88
- Misses 41762 41797 +35
Continue to review full report at Codecov.
|
tautschnig
force-pushed
the
dump-c-bool-constant
branch
from
06dd169 to
82d20b0
Compare
| irep | ||
| -- | ||
| Dump-c previously always generated 0 for _Bool or __CPROVER_bool-typed | ||
| constants. This test ensures that the value "1" is correctly generated. |
There was a problem hiding this comment.
I don't understand how this test tests this?
There was a problem hiding this comment.
Yeah... I'm not seeing it either. Not quite sure where the irep is coming from.
There was a problem hiding this comment.
Test description expanded: the previous (buggy) output made dump-c produce v = 0 instead of v = 1.
| @@ -1521,22 +1521,48 @@ void dump_ct::cleanup_type(typet &type) | |||
| !type.get(ID_tag).empty()); | |||
| } | |||
|
|
|||
| static expr2c_configurationt expr2c_configuration() | |||
| { | |||
| static expr2c_configurationt configuration{ | |||
There was a problem hiding this comment.
IMHO would be better written as a series of assignments, then you don't need the comments.
| @@ -156,7 +152,7 @@ class dump_ct | |||
| symbol_tablet copied_symbol_table; | |||
| const namespacet ns; | |||
| const dump_c_configurationt dump_c_config; | |||
| std::unique_ptr<languaget> language; | |||
| const irep_idt mode; | |||
There was a problem hiding this comment.
This change should be a separate commit with an explanation for why it's done. It's not obvious to me that this is an improvement, and in any case it doesn't seem to be directly related to fixing anything with the output of booleans? Not saying I'm against this, just that the commit should do a better job of explaining it.
There was a problem hiding this comment.
Broken out into a second commit.
| irep | ||
| -- | ||
| Dump-c previously always generated 0 for _Bool or __CPROVER_bool-typed | ||
| constants. This test ensures that the value "1" is correctly generated. |
There was a problem hiding this comment.
Yeah... I'm not seeing it either. Not quite sure where the irep is coming from.
| @@ -526,7 +526,7 @@ void dump_ct::convert_compound( | |||
| if(t.get_width()<=config.ansi_c.long_long_int_width) | |||
| struct_body << "long long int " << comp_name | |||
| << " : " << t.get_width(); | |||
| else if(language->id()=="cpp") | |||
| else if(mode == ID_cpp) | |||
There was a problem hiding this comment.
Doesn't seem to correspond with the PR message. I'm fine with them going in as a minor fix but just wanted to flag it in case it was a mistake.
tautschnig
force-pushed
the
dump-c-bool-constant
branch
2 times, most recently
from
9c881b0 to
167877a
Compare
tautschnig
force-pushed
the
dump-c-bool-constant
branch
from
167877a to
d95a0d0
Compare
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.
This avoids working around expr2c internals.
tautschnig
force-pushed
the
dump-c-bool-constant
branch
from
d95a0d0 to
1828d43
Compare
The CSmith test generated with random seed 1614606277 demonstrated that dump-c's handling still didn't cover all cases of byte_update expressions introduced by the C front-end, specifically missing the case where a struct was part of the union.
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.