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

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