MIR: Support raw pointer types #1977
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
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 theread_volatile
andwrite_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.The text was updated successfully, but these errors were encountered: