Skip to content

Refactor bmct into a more convenient API #15

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
Closed
peterschrammel opened this issue Mar 7, 2016 · 3 comments
Closed

Refactor bmct into a more convenient API #15

peterschrammel opened this issue Mar 7, 2016 · 3 comments
Assignees
@peterschrammel
Labels
enhancement Symbolic Execution

Comments

@peterschrammel
Copy link
Member

bmct and incremental_bmct can be easily used interchangeably in other BMC-based tools (like cegis)
most of that has already been done in the peter-incremental-unwinding branch
@peterschrammel peterschrammel self-assigned this Mar 7, 2016
@peterschrammel
Copy link
Member Author

Also @karkhaz's path-explorer needs to be separated out and based on a common safety-checker/BMC interface. The current integration into bmct itself is very hard to maintain.

@karkhaz
Copy link
Collaborator

karkhaz commented Jul 2, 2018

@peterschrammel bmct is certainly more unwieldy and less elegant than it used to be given the path explorer stuff, sorry about that. Is there anything specific that you'd like me to do or help with? I won't be free to work on CBMC for the next month or so, but if you have some specific suggestions I can start thinking about how to get them done.

@peterschrammel peterschrammel mentioned this issue Sep 11, 2018
Closed
@peterschrammel
Copy link
Member Author

has been done

zlfben pushed a commit to zlfben/cbmc that referenced this issue May 13, 2021
Merge pull request diffblue#15 from lefanz-amazon/lefan-abstraction
0f9b08c 
abst_read: implement and test abst plus/minus
TGWDB pushed a commit to TGWDB/cbmc that referenced this issue Jul 2, 2021
@thomasspriggs
Merge pull request diffblue#15 from thomasspriggs/tas/no_values_of_qu…
dcc7498 
…antifiers

Fix errors from issue 5970
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@peterschrammel peterschrammel

Labels
enhancement Symbolic Execution
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@karkhaz @peterschrammel