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

Specification refinement #1692

Merged
merged 3 commits into from
Jun 22, 2022
Merged

Specification refinement #1692

merged 3 commits into from
Jun 22, 2022

Conversation

robdockins
Copy link
Contributor

CF #1677

@robdockins robdockins force-pushed the rwd/spec-refinement branch from 24def9b to 63c6a0f Compare June 21, 2022 21:19
@robdockins
Implement llvm_refine_spec, which allows users to assemble a collec…
8abb56c 
…tion

of already-proved specifications for a function into a single
specification, or to logically restate the conditions of a specification.
@robdockins robdockins force-pushed the rwd/spec-refinement branch from 63c6a0f to f55c265 Compare June 21, 2022 21:19
@robdockins robdockins marked this pull request as ready for review June 21, 2022 21:20
@robdockins robdockins requested a review from chameco June 21, 2022 21:20
chameco
chameco approved these changes Jun 21, 2022
View reviewed changes
Copy link
Contributor

@chameco chameco left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, this looks great overall - it's very cool that we can reuse the existing methodSpecHandler infrastructure for this.

src/SAWScript/Crucible/LLVM/Builtins.hs Outdated Show resolved Hide resolved
src/SAWScript/Crucible/LLVM/Builtins.hs Outdated Show resolved Hide resolved
src/SAWScript/Crucible/LLVM/Builtins.hs Outdated Show resolved Hide resolved
src/SAWScript/Crucible/LLVM/Builtins.hs Outdated Show resolved Hide resolved
src/SAWScript/Crucible/LLVM/Builtins.hs Outdated Show resolved Hide resolved
src/SAWScript/Crucible/LLVM/Builtins.hs Outdated Show resolved Hide resolved
@robdockins robdockins force-pushed the rwd/spec-refinement branch from f55c265 to ee89fd6 Compare June 22, 2022 17:37
@robdockins robdockins added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Jun 22, 2022
@robdockins robdockins mentioned this pull request Jun 22, 2022
Open
@mergify mergify bot merged commit f6c58db into master Jun 22, 2022
@mergify mergify bot deleted the rwd/spec-refinement branch June 22, 2022 19:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@chameco chameco chameco approved these changes

Assignees
No one assigned
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@robdockins @chameco