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.

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

C heap tactic #507

Draft
wants to merge 6 commits into
base: master
Choose a base branch
from
Draft

Conversation

simonjwinwood
Copy link

This tactic deals with heap updates in the context of lift_t, turning UMM heap_updates into function updates to the lift_t, or removing them completely if the update doens't interact with the lift_t'd type.

simonjwinwood and others added 6 commits July 25, 2022 23:55
This tactic deals with lift_t/heap_update and friends, by examining
the type information discovered during C parsing.  The new tactic adds
new goals stating that the updates are OK, and then uses this
information to simplify the goal.
Not sure why this is required, but it keeps Isabelle happy.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants