Heapster Array Prover Redux #1617
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Contributor
abakst
commented
Mar 16, 2022
abakst
commented
- Reimplementation of Array prover logic in Heapster
- Adds test framework for Heapster implication prover plus Array testcases
abakst
changed the title
| @@ -1912,7 +1925,11 @@ simplImplIn (SImpl_LLVMArrayReturn x ap ret_ap) = | |||
| distPerms2 x (ValPerm_Conj [Perm_LLVMArray ret_ap]) | |||
| x (ValPerm_Conj [Perm_LLVMArray ap]) | |||
| else | |||
| error "simplImplIn: SImpl_LLVMArrayReturn: array not being borrowed or not a sub-array" | |||
| error ("simplImplIn: SImpl_LLVMArrayReturn: array not being borrowed or not a sub-array:\n" ++ | |||
| renderDoc ( | |||
There was a problem hiding this comment.
Small nitpick, but maybe put the entire renderDoc call on one line?
There was a problem hiding this comment.
Actually I had only added this for my own debugging and missed it when I initially reviewed the diffs. @eddywestbrook do you think it's useful to leave in, given that it has to use emptyPPInfo?
There was a problem hiding this comment.
You're right, you should just take it out
abakst
commented
Mar 22, 2022
abakst
commented
Mar 22, 2022
eddywestbrook
approved these changes
Mar 28, 2022
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.