Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Re-implement Heapster Coq Proof Automation #2026

Open
eddywestbrook opened this issue Feb 9, 2024 · 0 comments
Open

Re-implement Heapster Coq Proof Automation #2026

eddywestbrook opened this issue Feb 9, 2024 · 0 comments
Labels
subsystem: heapster Issues specifically related to memory verification using Heapster tech debt Issues that document or involve technical debt type: bug Issues reporting bugs or unexpected/unwanted behavior
Milestone
Someday

Comments

@eddywestbrook
Copy link
Contributor

All of the Coq proofs in the _proofs.v files in the heapster-saw/examples directory are now commented out, because they no longer work. This is in turn because PR #2017 updated the Coq definition of the SpecM monad to match this PR in the entree-specs repo, and the proof automation has not been updated in this new version of SpecM.

This is also discussed as an issue in the entree-specs repo.
@eddywestbrook eddywestbrook added the subsystem: heapster Issues specifically related to memory verification using Heapster label Feb 10, 2024
@sauclovian-g sauclovian-g added type: bug Issues reporting bugs or unexpected/unwanted behavior tech debt Issues that document or involve technical debt labels Nov 8, 2024
@sauclovian-g sauclovian-g added this to the Someday milestone Nov 8, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
subsystem: heapster Issues specifically related to memory verification using Heapster tech debt Issues that document or involve technical debt type: bug Issues reporting bugs or unexpected/unwanted behavior
Projects
None yet
Milestone
Someday
Development

No branches or pull requests
2 participants
@eddywestbrook @sauclovian-g