Heapster: improved bitvector and automation support #1792

Merged

eddywestbrook merged 5 commits intomasterfrom heapster-sha512

Jan 3, 2023

+271-233

Commits on Jan 3, 2023

Heapster: Support negating bitvector permission expressions
RyanGlScott
committed
added castVecS

Eddy Westbrook
authored and
RyanGlScott
committed
fixed the translation of the SImpl_LLVMArrayEmpty rule to produce a well-typed term

Eddy Westbrook
authored and
RyanGlScott
committed
changed implication prover for field permissions so that a field can be proved by a block that could contain its offset, rather that requiring it to definitely contain its offset

Eddy Westbrook
authored and
RyanGlScott
committed
add maybe automation to SpecMExtra

m-yac
authored and
RyanGlScott
committed