format(expr) beautification for quantifiers and = on booleans #2978
Conversation
kroening
requested review from
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
kroening
force-pushed
the
format_expr_beautification
branch
from
fa434a5 to
3629a4a
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: fa434a5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85166064
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 3629a4a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85169864
src/util/format_expr.cpp
Outdated
| else if(src.id() == ID_equal) | ||
| { | ||
| if(!src.operands().empty() && src.op0().type().id() == ID_bool) | ||
| operator_str = u8"\u21d4"; // <=>, U+21D4 |
There was a problem hiding this comment.
I think this would confuse someone using the output to debug, since they'd go looking for ID_iff
There was a problem hiding this comment.
It's used only four times across the code base, that makes for an almost trivial PR.
kroening
force-pushed
the
format_expr_beautification
branch
from
3629a4a to
be0aa32
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: be0aa32).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85359340
This makes the output closer to usual mathematical convention.
This makes the output closer to usual mathematical convention.
kroening
force-pushed
the
format_expr_beautification
branch
from
be0aa32 to
37f5b8e
Compare
There was a problem hiding this comment.
The fact that user-visible output changes but no changes to tests were necessary implies that we don't actually test this code. This might change if #2977 were merged, so let's get that merged first.
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 37f5b8e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85388192
|
@tautschnig This is now somewhat circular: to get #2977 merged, a lot of tests need to pass, and it's easier to achieve that if the output of format() is moved to be more similar to that what's there right now. |
No description provided.