Proc-assertions is a proc-macro tool built on Rust compiler. It laverages procedural assumptions to parse in compile-time object ASTs and inject assertion fragments based on the user request. Developed by Efficient Computing Lab for the TheseusOS verification purposes. Find previous commits here.

Installation

This crate is available on crates.io and can be used by adding the following to your project's Cargo.toml:

[dependencies]
proc_assertions = "0.1.1"

and this to your crate root (main.rs or lib.rs):

#[macro_use]
extern crate proc_assertions;

Usage

This crate exposes the following proc-macros:

• #[calls]
• #[nocalls]
• #[mutates]
• #[nomutates]
• #[private_fields]
• #[size_align]
• #[consumes]

For further details, please refer to the documentation.

FAQ

• Contributions are welcome via pull requests to the GitHub repository.
• These assertions are only used at compile-time and don't affect the final binary.
• There may be a slight increase in compile times due to additional assertions.
• Install rust-analyzer that employs notify::Watcher for real-time code monitoring.

License

This project is licensed under the MIT License.