-
Notifications
You must be signed in to change notification settings - Fork 274
Factor out show_vcc from bmct #2884
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
Conversation
4804ee0
to
16264b0
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.
+1 for moving it to goto-symex - the code depends on an implementation detail (symex_target_equation.h) of goto-symex.
16264b0
to
a1c327a
Compare
@tautschnig, moved. |
a1c327a
to
5f26ece
Compare
@@ -69,7 +69,6 @@ BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \ | |||
../src/cbmc/cbmc_solvers$(OBJEXT) \ | |||
../src/cbmc/counterexample_beautification$(OBJEXT) \ | |||
../src/cbmc/fault_localization$(OBJEXT) \ | |||
../src/cbmc/show_vcc$(OBJEXT) \ |
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.
is the moved one not needed here ?
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.
The moved one is dragged in implicitly via goto-symex$(LIBEXT)
.
5f26ece
to
795e988
Compare
Based on #2883Only review last commitCould also be moved to goto-symex [done]