Open
Description
Context
- RustWeek - All Hands - Naming safety requirements & invariants (2025.05)
- Rust Safety Standard - Increasing the Correctness of unsafe Code (2024.09)
- RFC PATCH 0/5 Introduce the Rust Safety Standard (2024.07)
- Safety comments and atomicity requirements (2024.03)
Idea
Since tag-std currently is a PoC, there are several ways to apply it to R4L
- write a universal tool that can apply to any Rust project
- or enhance klint a static analysis tool/infrastructure in R4L
- or write a universal library that can be shared in different workflows/tools
- Feat: add tag-std and cargo-tag-std demo by driving rustc #1 demonstrates a normal workflow for single file and most cargo-based projects
- libstd needs a workflow: Black arts of verifying libcore/libstd os-checker/distributed-verification#52
- R4L needs its own: klint can reuse the library
- the main downside is multi-toolchains problem: StableMir should ideally solve this
cc #2
#![register_tool(klint)]
#[klint::NotNull(self.ptr)]
unsafe fn foo(&self) { ... }
Metadata
Metadata
Assignees
Labels
No labels