Module remove_dynamic_checks

Micro-pass: remove the dynamic checks for array/slice bounds, overflow, and division by zero.

Note that from a semantic point of view, an out-of-bound access or a division by zero must lead to a panic in Rust (which is why those checks are always present, even when compiling for release). In our case, we take this into account in the semantics of our array/slice manipulation and arithmetic functions, on the verification side.

Structs

Transform

Functions

equiv_op 🔒

Check if the two operands are equivalent: either they’re the same constant, or they represent the same place (regardless of whether the operand is a move or a copy)

make_binop_overflow_panic 🔒

make_unop_overflow_panic 🔒

remove_dynamic_checks 🔒

Rustc inserts dynamic checks during MIR lowering. They all end in an Assert statement (and this is the only use of this statement).

uses_local 🔒

Whether the value uses the given local in a place.