-
Notifications
You must be signed in to change notification settings - Fork 274
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
Move cbmc/bmc and all_properties to jbmc #4217
Conversation
54f8084
to
8234d57
Compare
There was a problem hiding this 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.
Remove obsolete cbmc/bmc_cover [blocks: #4217]
8234d57
to
0965290
Compare
ca29ac7
to
9195c9c
Compare
There was a problem hiding this 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.)
These aren't used by CBMC anymore, but only for the symex-driven lazy-loading mode of JBMC.
Cannot use deprecated bmct anymore.
9195c9c
to
14109a4
Compare
These classes aren't used by CBMC anymore.
Based on #4216 - last 3 commits