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

Allow printing of SetupValues #215

Closed
jldodds opened this issue Jul 11, 2017 · 3 comments
Closed

Allow printing of SetupValues #215

jldodds opened this issue Jul 11, 2017 · 3 comments
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm usability An issue that impedes efficient understanding and use wontfix Closed issues that we decided not to fix, but are still potentially relevant

Comments

@jldodds
Copy link
Contributor

jldodds commented Jul 11, 2017

Previous behavior printed counter examples in an "encountered, expected" format. When a proof fails it would be particularly useful to see the counterexample in the state where the assertion is checked, in particular for the LLVM, which is often harder to run outside of SAW. A straightforward way of achieving this without making default prints too verbose might be to allow the printing of SetupValues.

@langston-barrett
Copy link
Contributor

@jldodds We can now print SetupValues, can you elaborate a bit on "see the counterexample in the state where the assertion is checked"?

@langston-barrett langston-barrett added the subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm label Jun 24, 2019
@atomb atomb added the usability An issue that impedes efficient understanding and use label Apr 28, 2020
@atomb atomb added this to the 0.6 milestone May 5, 2020
@brianhuffman
Copy link
Contributor

Here's my understanding of what the problem is: If you have a C program containing an assertion like assert(x < 10), and that assertion fails, then just printing a list of the initial values of the function arguments is insufficient; we really would like to see the value of x as well.

@atomb atomb modified the milestones: 0.6, 0.7 Aug 20, 2020
@atomb atomb removed this from the 0.7 milestone Oct 16, 2020
@atomb atomb added the wontfix Closed issues that we decided not to fix, but are still potentially relevant label Oct 16, 2020
@atomb
Copy link
Contributor

atomb commented Oct 16, 2020

This will be subsumed by other work and doesn't have much explanation included that we need to keep track of.

@atomb atomb closed this as completed Oct 16, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm usability An issue that impedes efficient understanding and use wontfix Closed issues that we decided not to fix, but are still potentially relevant
Projects
None yet
Development

No branches or pull requests

4 participants