Skip to content

Use CPROVER_PREFIX macro instead of hardcoded __CPROVER_ string #3171

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 3 commits into from
Oct 29, 2018
Merged

Use CPROVER_PREFIX macro instead of hardcoded __CPROVER_ string #3171

merged 3 commits into from
Oct 29, 2018

Conversation

tautschnig
Copy link
Collaborator

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

  • Each commit message has a non-empty body, explaining why the change was made.
  • My contribution is formatted in line with CODING_STANDARD.md.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj
allredj reviewed Oct 15, 2018
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Passed Diffblue compatibility checks (cbmc commit: 836af2c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87932897

thk123
thk123 approved these changes Oct 15, 2018
View reviewed changes
Copy link
Contributor

@thk123 thk123 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What a terrifying number of magic strings duplicated everywhere, this is certainly an improvement though.

src/goto-programs/slice_global_inits.cpp Outdated
@@ -43,7 +43,8 @@ void slice_global_inits(goto_modelt &goto_model)
call_grapht::create_from_root_function(goto_model, entry_point, false);
const auto directed_graph = call_graph.get_directed_graph();
INVARIANT(
!directed_graph.empty(), "At least __CPROVER_start should be reachable");
!directed_graph.empty(),
"at least " CPROVER_PREFIX "start should be reachable");
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ goto_functionst::entry_point() inplace of it all if anything

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good one, because also that one was always wrong: it was missing an extra underscore...

chrisr-diffblue
chrisr-diffblue approved these changes Oct 15, 2018
View reviewed changes
Copy link
Contributor

@chrisr-diffblue chrisr-diffblue left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

@tautschnig tautschnig requested a review from forejtv as a code owner October 15, 2018 10:39
@tautschnig
Copy link
Collaborator Author

@chrisr-diffblue Linter check added.

@chrisr-diffblue
Copy link
Contributor

Thanks for the additional linter check @tautschnig - definitely LGTM now.

allredj
allredj reviewed Oct 15, 2018
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Passed Diffblue compatibility checks (cbmc commit: 21a5586).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87942241

allredj
allredj reviewed Oct 15, 2018
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Passed Diffblue compatibility checks (cbmc commit: d942999).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87943412

martin-cs
martin-cs approved these changes Oct 15, 2018
View reviewed changes
Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good, thanks for the clean up.

@tautschnig tautschnig mentioned this pull request Oct 15, 2018
Merged
3 tasks
allredj
allredj reviewed Oct 22, 2018
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Passed Diffblue compatibility checks (cbmc commit: 4da3fa5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88740531

@tautschnig
Use CPROVER_PREFIX macro instead of hardcoded __CPROVER_ string
4a02c75 
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
@tautschnig
Linter and clang-format ignores, and whitespace cleanup
0ce0ac2
@tautschnig
Check for uses of __CPROVER_ in the linter
3a67fb6 
This should help avoid future code introducing literal uses of __CPROVER_ back
into the code base.
@tautschnig tautschnig merged commit 3ab73ea into diffblue:develop Oct 29, 2018
@tautschnig tautschnig deleted the use_cprover_prefix branch October 29, 2018 18:52
allredj
allredj reviewed Oct 29, 2018
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🚫
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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@smowton smowton smowton approved these changes

@thk123 thk123 thk123 approved these changes

@kroening kroening kroening approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

@martin-cs martin-cs martin-cs approved these changes

@chrisr-diffblue chrisr-diffblue chrisr-diffblue approved these changes

@cesaro cesaro Awaiting requested review from cesaro

@cristina-david cristina-david Awaiting requested review from cristina-david

@NathanJPhillips NathanJPhillips Awaiting requested review from NathanJPhillips

@pkesseli pkesseli Awaiting requested review from pkesseli

@forejtv forejtv Awaiting requested review from forejtv

Assignees

@kroening kroening

Labels
cleanup
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Cleanup all literal uses of "__CPROVER_" and use CPROVER_PREFIX instead
9 participants
@tautschnig @chrisr-diffblue @smowton @thk123 @kroening @peterschrammel @martin-cs @allredj @pkesseli