--show-vcc now uses format() #2977
Conversation
kroening
requested review from
chrisr-diffblue,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
kroening
force-pushed
the
show-vcc-format
branch
3 times, most recently
from
669c607 to
145603c
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 145603c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85176699
| out << "GUARD: " << string_value << "\n"; | ||
| out << "\n"; | ||
| out << "GUARD: " << format(p_it->guard_expr) << '\n'; | ||
| out << '\n'; |
There was a problem hiding this comment.
Is there actually value in this? If there is, then it should likely be guarded by #ifdef DEBUG instead of #if 0
src/goto-symex/show_vcc.cpp
Outdated
| std::string string_value = | ||
| from_expr(ns, s_it->source.pc->function, s_it->cond_expr); | ||
| out << "{" << 1 << "} " << string_value << "\n"; | ||
| out << '{' << 1 << "} " << format(s_it->cond_expr) << '\n'; |
There was a problem hiding this comment.
How about out << "{1} " ... unless some magic is happening here?
kroening
force-pushed
the
show-vcc-format
branch
2 times, most recently
from
9f24f83 to
a74e051
Compare
There was a problem hiding this comment.
The changes in here all look good, but (as stated in #2978) changes to the output should really break some tests. Is it really the case that the output has not changed at all, despite now using unicode symbols for all sort of operators? I'd rather think that we are not testing this output anywhere, and this makes me nervous. I think there are already several regression tests using --show-vcc, but apparently these don't actually inspect the output.
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: a74e051).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85634310
kroening
force-pushed
the
show-vcc-format
branch
from
a74e051 to
8d3b637
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 8d3b637).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87640378
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).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
kroening
force-pushed
the
show-vcc-format
branch
2 times, most recently
from
5dded4a to
5fb0254
Compare
This outputs the verification conditions in 'first order logic syntax', as opposed to syntax used by a programming language, which may cause confusion.
kroening
force-pushed
the
show-vcc-format
branch
from
5fb0254 to
857797c
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 857797c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87897393
|
There's now a test that looks at the output. |
No description provided.