-
Notifications
You must be signed in to change notification settings - Fork 43
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
uc-crux-llvm: User-provided specifications for functions #1003
Conversation
60eb33a
to
3bdc429
Compare
3bdc429
to
4b07993
Compare
Rebased onto #1001. |
4b07993
to
4f5d70a
Compare
CI failure seems unrelated:
|
CI seems to be failing reliably at this step, though why that should be so for the Ubuntu 20.04/GHC 9.0.2 build and not the other Ubuntu 20.04 builds is a bit mystifying considering that this step doesn't involve GHC/Cabal. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't really have context for the UC-Crux changes, but the change to crucible proper seem fine to me.
26785db
to
ccf28f9
Compare
Still needs: - Code-level docs - User-facing docs - Integration with Loop - Integration with the CLI - Ideally, some tests
Make fields into a record type for extensibility and documentation
Still needs to be plumbed through to Loop.
So that these overrides can create new symbolic values that are tracked and understood by classification.
Make it a little more user friendly now that users have to write it (see --spec-path).
These test the semantics of the nondetBranches construct.
ccf28f9
to
979ddfb
Compare
Fixes #982. Based on #1001. Best place to start reviewing would probably be by reading the user-facing docs (rendered).