A demo to show how safety properties can be checked on unsafe Rust code.
Several projects are checked, while each project may pin own toolchain.
So to support them in the same tool, conditional compilation gated by --features is needed.
Projects and feature names:
| project | --features (or -F) |
|---|---|
| verify-rust-std | std |
| Rust for Linux | rfl |
| asterinas | asterinas |
There is no default toolchain for now, so one must set up it first and then build or install it.
For example, to check Rust for Linux codebase, specify rfl like this:
./gen_rust_toolchain_toml.rs rfl
cargo build -Frfl