Heapster: existential function output perms#1549

Merged

mergify[bot] merged 18 commits intomasterfrom heapster/existential-fun-out-perms

Dec 23, 2021

+1,071-679

Commits on Dec 15, 2021

changed function permissions to have existential variables on the output permissions
Eddy Westbrook
committed
added parsing support for existential output permissions in fun perms
Eddy Westbrook
committed
finished updating Implication.hs and RustTypes.hs to work with the new existential outputs in funperms
Eddy Westbrook
committed
whoops, small typo in the new def of AstFunPerm
Eddy Westbrook
committed
whoops, reassociated the output permissions of a FunPerm to associate gouts and ret together
Eddy Westbrook
committed

Commits on Dec 16, 2021

got TypedCrucible.hs updated with existential function outputs permissions
Eddy Westbrook
committed
small tweaks to fix compiler warnings
Eddy Westbrook
committed
started updating SAWTranslation.hs to handle existential function output permissions
Eddy Westbrook
committed

Commits on Dec 21, 2021

finished updating all of Heapster to work with existential function output permissions!
Eddy Westbrook
committed

Commits on Dec 22, 2021

started writing abstractFunVarsForLifetimes
Eddy Westbrook
committed
finished implementing abstractFunVarsForLifetimes
Eddy Westbrook
committed

Commits on Dec 23, 2021

fixed lownedPermVarAndPErm, lownedPermsVars, and lownedPermsToDistPerms to accommodate for offsets on variables, thereby removing errors when ending lifetimes with offset variables in the lowned pe…
Eddy Westbrook
committed
uncommented string_deref because now it works!
Eddy Westbrook
committed
Merge branch 'master' into heapster/existential-fun-out-perms
Eddy Westbrook
committed
Update heapster-saw/src/Verifier/SAW/Heapster/Parser.y

Eddy Westbrook
and
m-yac
authored
added comments to the components of the AstFunPerm type
Eddy Westbrook
committed
moved some helper functions to the top of RustTypes.hs and added comments to them
Eddy Westbrook
committed
whoops, forgot to update the output of the parsing rule that was changed on a previous commit
Eddy Westbrook
committed