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

Print less verbose information when LLVM simulation fails #162

Closed
atomb opened this issue Aug 2, 2016 · 1 comment
Closed

Print less verbose information when LLVM simulation fails #162

atomb opened this issue Aug 2, 2016 · 1 comment
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm topics: error-messages Issues involving the messages SAW produces on error type: enhancement Issues describing an improvement to an existing feature or capability
Milestone
0.7

Comments

@atomb
Copy link
Contributor

atomb commented Aug 2, 2016

Currently, if the symbolic simulation of an LLVM program fails, it prints out the entire symbolic state of the program, which can in come cases be extremely large. Generally much of this information isn't relevant. It may make sense to print less by default, and only print everything if specifically asked for.
@atomb atomb added the type: enhancement Issues describing an improvement to an existing feature or capability label May 2, 2017
@langston-barrett langston-barrett mentioned this issue Jun 24, 2019
Closed
@langston-barrett langston-barrett added subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm topics: error-messages Issues involving the messages SAW produces on error labels Jun 24, 2019
@atomb atomb added this to the 0.6 milestone Apr 24, 2020
@atomb atomb modified the milestones: 0.6, 0.7 Aug 6, 2020
@atomb
Copy link
Contributor Author

atomb commented Oct 16, 2020

This is partly fixed and subsumed by other planned work.

@atomb atomb closed this as completed Oct 16, 2020
brianhuffman pushed a commit that referenced this issue Apr 26, 2021
Replace GlobalDef term constructor with Primitive.
02f2be2 
The new `Primitive` constructor is for global constants that do
not have definitions. Instead of an `Ident`, they are identified
with an `ExtCns`, which includes a `NameInfo` and a type.

Fixes #162.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm topics: error-messages Issues involving the messages SAW produces on error type: enhancement Issues describing an improvement to an existing feature or capability
Projects
None yet
Milestone
0.7
Development

No branches or pull requests
2 participants
@atomb @langston-barrett