Improve Heapster implication prover for opaque named shapes#1394

Merged

eddywestbrook merged 5 commits intomasterfrom heapster-opaque-named-blocks

Jul 22, 2021

+52-17

Commits on Jul 20, 2021

Implement a command to introduce new SAWCore primitives via Heapster
ChrisEPhifer
committed

Commits on Jul 21, 2021

did some work to improve the implication prover for opaque named shapes, including: modalizeShape for opaque named shapes is now a no-op; and proveVarLLVMBlock now eliminates a perm on the LHS when…
Eddy Westbrook
committed

Commits on Jul 22, 2021

Merge remote-tracking branch 'origin/master' into heapster-opaque-named-blocks
Eddy Westbrook
committed
generated Coq file changed a bit
Eddy Westbrook
committed
small fix to comment
Eddy Westbrook
committed