Heapster: Add support for the trivially false permission#1543

Merged

ChrisEPhifer merged 21 commits intomasterfrom heapster/add-false-permission

Dec 20, 2021

+137-1

Commits on Dec 16, 2021

Oops, translation should be to FalseProp rather than the empty type
ChrisEPhifer
committed
Add a simple implication for eliminating false shapes
ChrisEPhifer
committed
Write a (dubiously correct) translation of false elimination to a functional form
ChrisEPhifer
committed
Support for recombination of blocks containing false shapes / application of false elimination implication rules
ChrisEPhifer
committed
Use the shiny new false shape for the Rust ! type
ChrisEPhifer
committed
Take a stab at laying out the false shape
ChrisEPhifer
committed
BROKEN: Add a test case for panic / never-typed Rust terms. Fails to typecheck currently
ChrisEPhifer
committed
Oops, Location is 16 bytes - doesn't fix our errors completely, though
ChrisEPhifer
committed

Commits on Dec 17, 2021

Manually provide the shape of Location; still has errors upon typechecking, though
ChrisEPhifer
committed

Commits on Dec 20, 2021

changed the translation of string constants to generate a sequence of byte-sized eq perms instead of one giant eq perm for the whole string, which seems to fix some endianness issues
Eddy Westbrook
committed