Use CPROVER_PREFIX macro instead of hardcoded __CPROVER_ string#3171
Use CPROVER_PREFIX macro instead of hardcoded __CPROVER_ string#3171tautschnig merged 3 commits intodiffblue:developfrom
Conversation
allredj
left a comment
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 836af2c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87932897
thk123
left a comment
There was a problem hiding this comment.
What a terrifying number of magic strings duplicated everywhere, this is certainly an improvement though.
| INVARIANT( | ||
| !directed_graph.empty(), "At least __CPROVER_start should be reachable"); | ||
| !directed_graph.empty(), | ||
| "at least " CPROVER_PREFIX "start should be reachable"); |
There was a problem hiding this comment.
⛏️ goto_functionst::entry_point() inplace of it all if anything
There was a problem hiding this comment.
Good one, because also that one was always wrong: it was missing an extra underscore...
chrisr-diffblue
left a comment
There was a problem hiding this comment.
Good to see this cleanup! Is it worth also adding a linter and/or clang-format rule to catch the use of raw magic __CPROVER_blah strings?
836af2c to
21a5586
Compare
|
@chrisr-diffblue Linter check added. |
|
Thanks for the additional linter check @tautschnig - definitely LGTM now. |
allredj
left a comment
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 21a5586).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87942241
allredj
left a comment
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: d942999).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87943412
martin-cs
left a comment
There was a problem hiding this comment.
Looks good, thanks for the clean up.
d942999 to
4da3fa5
Compare
allredj
left a comment
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 4da3fa5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88740531
Using string literals is prone to typos and sometimes, but not always, using the CPROVER_PREFIX macro removes the potential for central modifications. Fixes: diffblue#735
This should help avoid future code introducing literal uses of __CPROVER_ back into the code base.
4da3fa5 to
3a67fb6
Compare
allredj
left a comment
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 3a67fb6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/89554147
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.
Using string literals is prone to typos and sometimes, but not always, using the CPROVER_PREFIX macro removes the potential for central modifications.
Fixes: #735