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

Heapster fix lowned proofs #1415

Merged
merged 34 commits into from
Aug 11, 2021
Merged

Heapster fix lowned proofs #1415

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
34 commits
Select commit Hold shift + click to select a range
9b91107
added ppInfoAddTypedExprNames to use a base name for each variable de…
Jul 28, 2021
7b2b709
whoops, fixed an infinite loop
Jul 28, 2021
6af2bd5
implemented lifetime subsumption
Jul 28, 2021
fd00a6d
started adding a new version of lowned permissions that include a not…
Jul 30, 2021
71b0535
bugfix: there was an infinite loop that kept copying a block permissi…
Aug 3, 2021
ffc7e85
added debug output for return statements, which is long overdue
Aug 3, 2021
f41437b
changed implElimLLVMBlock to always only eliminate one step of a memb…
Aug 3, 2021
465194b
unfold defined shapes on the left when their ranges match a shape we …
Aug 3, 2021
aa63297
whoops, do not try to eliminate LHS block perms when we are proving a…
Aug 3, 2021
9f27cc6
added a case to proveVarLLVMBlocks to detect if the right-hand side i…
Aug 4, 2021
413ff46
added another special case to proveVarLLVMBlocks, to eliminate a sequ…
Aug 4, 2021
d03220b
Merge remote-tracking branch 'origin/master' into heapster-memblock-p…
Aug 5, 2021
36f9a57
Merge branch 'heapster-lifetime-subsumption' into heapster-memblock-p…
Aug 5, 2021
da20fb7
finished updating Implication.hs with the new lowned permission form
Aug 6, 2021
ea196ef
reorganized proveVarLLVMBlocks into two separate stages represented b…
Aug 6, 2021
676c07f
whoops, forgot to change a shadowed variable...
Aug 6, 2021
ed50023
implemented a few more suggestions from Eric Mertens
Aug 6, 2021
d8a8152
Merge branch 'heapster-memblock-prover-improvements' into heapster-li…
Aug 6, 2021
5a16391
fixed an infinite loop in proving the new lowned permissions; also ad…
Aug 6, 2021
820b846
updated the translation for the new lfinished permission and the modi…
Aug 6, 2021
1312374
updated the remaining Heapster files to reflect the new form of the l…
Aug 6, 2021
69a272e
added parser support for lfinished perms and for lowned perms with n…
Aug 6, 2021
7934d72
Merge remote-tracking branch 'origin/master' into heapster-lifetime-s…
Aug 9, 2021
91e4e9a
whoops, fixed the parser rules for an optional list of lifetimes
Aug 9, 2021
a1a1f68
trying out a new approach for proving lowned permissions: instead of …
Aug 9, 2021
84dbd11
fixed localProveVars to recombine the input permissions in reverse or…
Aug 10, 2021
0322bea
changed instantiateLifetimeVars to explicitly look for lowned permiss…
Aug 10, 2021
d71ae9b
changed implEndLifetimeRecM to no longer leave the lfinished permissi…
Aug 10, 2021
22ebbb6
added a case to simplify1PermForDetVars to end any indetermined lifet…
Aug 10, 2021
be13023
Merge remote-tracking branch 'origin/master' into heapster-fix-lowned…
Aug 10, 2021
791b64b
Merge remote-tracking branch 'origin/master' into heapster-fix-lowned…
Aug 10, 2021
bb1122a
whoops, fixed comments
Aug 10, 2021
ef3efc2
retrigger the CI checks
Aug 11, 2021
0900364
updated arrays.v with its new translation
Aug 11, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading