Make lifetimesThatCouldProve more precise#1667

Merged

mergify[bot] merged 10 commits intomasterfrom heapster/debug-recombine-perm

May 18, 2022

+369-94

Commits on May 5, 2022

changed recombinePerm to not eliminate a block permission whose range overlaps with another permission that is already held; fixed a bug in the logic for proving lcurrent permissions to avoid a lif…
Eddy Westbrook
committed
Merge branch 'master' into heapster/debug-recombine-perm
Eddy Westbrook
committed

Commits on May 6, 2022

added equality casting to lifetimesThatCouldProve, with the result that too many lifetimes are ended
Eddy Westbrook
committed

Commits on May 11, 2022

added a debug print statement to tcTranslateCFGTupleFun to print out the type being used for a function when it is type-checked at debug level
Eddy Westbrook
committed

Commits on May 13, 2022

Commits on May 16, 2022

Merge branch 'master' into heapster/debug-recombine-perm
Eddy Westbrook
committed

Commits on May 17, 2022

changed lifetimesThatCouldProve to also check if a variable that is returned by a lifetime is in a contained eq permission of a permission we currently hold on a variable on the right
Eddy Westbrook
committed

Commits on May 18, 2022

removed debug tracing
Eddy Westbrook
committed
removed an old non-exhaustive pattern-matching warning
Eddy Westbrook
committed