Add way to have irep pretty printed as diagnostic #2930
Conversation
hannes-steffenhagen-diffblue
requested review from
kroening,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
hannes-steffenhagen-diffblue
force-pushed
the
feature-irep_diagnostic
branch
from
660fdd7 to
969825c
Compare
src/util/irep.h
Outdated
| struct irep_pretty_diagnosticst | ||
| { | ||
| const irept &irep; | ||
| }; |
There was a problem hiding this comment.
Can we have a constructor that takes const irept &irep?
There was a problem hiding this comment.
Done
hannes-steffenhagen-diffblue
force-pushed
the
feature-irep_diagnostic
branch
from
969825c to
3a59bd6
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 969825c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84317430
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).
src/util/irep.cpp
Outdated
| : irep(irep) | ||
| { | ||
| } | ||
|
|
| Invariant check failed | ||
| value: 00000000000000000000000000001000 | ||
| value: 00000000000000000000000000001101 | ||
|
|
regression/invariants/driver.cpp
Outdated
| @@ -149,6 +152,13 @@ int main(int argc, char** argv) | |||
| "an invariant with some custom diagnostics", | |||
| DiagnosticA{}, | |||
| DiagnosticB{}); | |||
| else if(arg == "invariant-with-irep-diagnostics") | |||
| INVARIANT_WITH_DIAGNOSTICS( | |||
There was a problem hiding this comment.
put multi-line statement inside braces.
hannes-steffenhagen-diffblue
force-pushed
the
feature-irep_diagnostic
branch
from
3a59bd6 to
1ba1da2
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 3a59bd6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84330448
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: 1ba1da2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84331624
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 1ba1da2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84412314
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.
This PR failed Diffblue compatibility checks (cbmc commit: 1ba1da2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84412314
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).
|
Merging despite compatibility check as per in-person communication with @thk123 |
Note that this is done through a wrapper to easily allow switching between different ways to represent an irep, here it's done with
pretty(), but depending on the irep other representations (such asfrom_expr) or a combination of different representations may be desirable.