pub trait HasSafety {
// Required method
fn safety(&self, krate: &TranslatedCrate) -> Safety;
}Expand description
The safety of evaluating this, following the rules outlined in https://doc.rust-lang.org/book/ch20-01-unsafe-rust.html and https://doc.rust-lang.org/reference/unsafety.html.
This is computed on the translated (U)LLBC, so it can’t know exactly what the user wrote. For example,
macros like println!("{x}") expand to unsafe operations inside their own unsafe blocks. Some safe
operations like slice indexing also expand to a bounds check followed by an unchecked access. Dead code
elimination may hide an unsafe operation. So all in all this will not report exactly the same safety as
rustc sees in the surface code. It is however accurate if you treat (U)LLBC as its own language: we
accurately flag operations that have soundness preconditions.
We currently don’t support unsafe fields and unsafe binders.
Required Methods§
fn safety(&self, krate: &TranslatedCrate) -> Safety
Dyn Compatibility§
This trait is dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety".
Implementors§
impl HasSafety for AbortKind
impl HasSafety for BinOp
impl HasSafety for BorrowckStatement
impl HasSafety for Call
The safety of calling the function (see CallSafety) and of evaluating the function pointer,
the operands and the destination.
impl HasSafety for FnOperand
impl HasSafety for FunSig
impl HasSafety for Operand
impl HasSafety for OverflowMode
impl HasSafety for Rvalue
impl HasSafety for charon_lib::ast::bodies::structured::Statement
This doesn’t look into nested blocks.
impl HasSafety for charon_lib::ast::bodies::unstructured::Statement
Note that calls are terminators.