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.

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

slice-formula is enabled unconditionally, but should not be used when getting traces #1288

Closed
tedinski opened this issue Jun 17, 2022 · 0 comments · Fixed by #1479
Closed

slice-formula is enabled unconditionally, but should not be used when getting traces #1288

tedinski opened this issue Jun 17, 2022 · 0 comments · Fixed by #1479
Assignees
@jaisnan

Comments

@tedinski
Copy link
Contributor

CBMC's --slice-formula can result in bizarre traces with weird values being assigned to variables CBMC no longer considers important.

We should not enable it when we're generating traces.

We should also have a flag that allows disabling it (--no-slice-formula?)
@jaisnan jaisnan self-assigned this Jul 27, 2022
@jaisnan jaisnan added this to Kani v0.8 Aug 2, 2022
@jaisnan jaisnan moved this to In Progress in Kani v0.8 Aug 2, 2022
@sanjit-bhat sanjit-bhat mentioned this issue Aug 5, 2022
Merged
4 tasks
@jaisnan jaisnan mentioned this issue Aug 9, 2022
Merged
4 tasks
Repository owner moved this from In Progress to Done in Kani v0.8 Aug 9, 2022
@celinval celinval mentioned this issue Aug 9, 2022
Open
6 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@jaisnan jaisnan

Labels
None yet
Projects
No open projects
Kani v0.8
Status: Done
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Disable calling --slice-formula by default with conditional flags. jaisnan/kani
2 participants
@tedinski @jaisnan