Skip to content
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

Variables irrelevant to the failure are not part of the trace #56

Open
prapicault opened this issue Dec 18, 2014 · 0 comments
Open

Variables irrelevant to the failure are not part of the trace #56

prapicault opened this issue Dec 18, 2014 · 0 comments

Comments

@prapicault
Copy link
Contributor

The counter examples produced by CBMC omit variables that are not relevant to reproduction of the problem. At first this could be confusing to the users.
In order to improve the situation, CBMC could have a mode that produces "special" assignments for these irrelevant variables (e.g. where the value is "variable not needed for counter example") and those could then be shown in the debugger.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant