Skip to content

Move cbmc/bmc and all_properties to jbmc #4217

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.

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

Merged
merged 3 commits into from
Mar 21, 2019

Conversation

peterschrammel
Copy link
Member

@peterschrammel peterschrammel commented Feb 18, 2019

These classes aren't used by CBMC anymore.

Based on #4216 - last 3 commits

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • 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).
  • 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.

Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

I think "Remove obsolete unit test" is neither true nor should it actually happen: the unit test remains as important, I don't think it is obsolete at all. If it uses an interface that's not the current one then it needs to be adapted. This may be non-trivial, but especially these tests are really important. If the new interface makes it somehow impossible to adapt the test then we've got a problem, because it means we have arrived at a black-box that prohibits testing.

tautschnig added a commit that referenced this pull request Mar 4, 2019
Remove obsolete cbmc/bmc_cover [blocks: #4217]
@peterschrammel peterschrammel changed the title Move cbmc/bmc and all_properties to jbmc [depends: 4216] Move cbmc/bmc and all_properties to jbmc Mar 17, 2019
@peterschrammel peterschrammel force-pushed the move-bmct-jbmc branch 3 times, most recently from ca29ac7 to 9195c9c Compare March 17, 2019 19:53
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

Thank you for updating the unit test! (But it does still require a rebase.)

@tautschnig tautschnig removed their assignment Mar 21, 2019
These aren't used by CBMC anymore, but only
for the symex-driven lazy-loading mode of JBMC.
Cannot use deprecated bmct anymore.
@peterschrammel peterschrammel merged commit 2e04b54 into diffblue:develop Mar 21, 2019
@peterschrammel peterschrammel deleted the move-bmct-jbmc branch March 21, 2019 14:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants