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

MIR: Support raw pointer types #1977

Open
RyanGlScott opened this issue Nov 13, 2023 · 0 comments
Open

MIR: Support raw pointer types #1977

RyanGlScott opened this issue Nov 13, 2023 · 0 comments
Labels
subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json type: enhancement Issues describing an improvement to an existing feature or capability

Comments

@RyanGlScott
Copy link
Contributor

The SAW MIR backend currently supports writing specifications involving reference types, but it does support specifications involving raw pointer types (e.g., *const T or *mut T). This would be of benefit for certain classes of unsafe code. In particular, it is important to support the read_volatile and write_volatile functions, which are used for ensuring memory sanitization. (See also GaloisInc/crucible#1130, which would be a prerequisite.)

Note that crucible-mir itself already supports raw pointer types, so fixing this issue would likely be a simple matter of determining what API we want to offer in SAW to interface with raw pointers.

@RyanGlScott RyanGlScott added type: enhancement Issues describing an improvement to an existing feature or capability subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json labels Nov 13, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json type: enhancement Issues describing an improvement to an existing feature or capability
Projects
None yet
Development

No branches or pull requests

1 participant