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

More Heapster rust typechecking bugs #1525

Merged
merged 6 commits into from
Nov 30, 2021

Conversation

eddywestbrook
Copy link
Contributor

This PR includes the following changes in support of type-checking LLVM compiled from Rust:

  • bugfix: proveVarLLVMBlocks was incorrectly setting the size of the field to prove when proving a memblock with variable shape from a field that did not start at the same offset

  • added the heapster_find_symbol_with_type and heapster_find_symbols_with_type commands to use LLVM types when searching for symbols

  • added the heapster_find_symbol_commands command to automatically generate heapster_find_symbol_with_type commands for the symbols in a particular file, to make it easier for the user to write them

Copy link
Member

@ChrisEPhifer ChrisEPhifer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Everything looks good to me! These commands are going to be super helpful to avoid undue proof-sensitivity.

@eddywestbrook eddywestbrook added subsystem: heapster Issues specifically related to memory verification using Heapster PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run labels Nov 30, 2021
@mergify mergify bot merged commit 19b2a79 into master Nov 30, 2021
@mergify mergify bot deleted the heapster/rust-typechecking-bugs-pr2 branch November 30, 2021 20:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run subsystem: heapster Issues specifically related to memory verification using Heapster
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants