rapx/cli/
verify.rs

1use clap::Args;
2
3#[derive(Debug, Clone, Copy, clap::ValueEnum)]
4pub enum VerifyMode {
5    #[value(help = "Auto-detect: verify all functions with unsafe callees or struct invariants")]
6    Scan,
7    #[value(help = "Only verify functions annotated with #[rapx::verify]")]
8    Targeted,
9    #[value(help = "Like `scan` or `targeted` but skip struct invariant checks")]
10    Invless,
11}
12
13/// Arguments for the `verify` command.
14#[derive(Debug, Clone, Args)]
15pub struct VerifyArgs {
16    /// Identify all functions annotated with #[rapx::verify] and print each target, its unsafe callees, and their safety contracts.
17    #[arg(long)]
18    pub prepare_targets: bool,
19    /// Number of extra SCC postfix repetitions allowed during path enumeration.
20    /// Default is 0 (postfix segments appear once each). Set to 1 to allow one extra repetition (two total occurrences), etc.
21    #[arg(long, default_value_t = 0)]
22    pub postfix_repeat: usize,
23    /// Verification mode: `scan` auto-detects unannotated unsafe targets (default), `targeted` verifies #[rapx::verify] functions.
24    #[arg(long, default_value = "scan")]
25    pub mode: VerifyMode,
26    /// Filter verification targets to only those within the specified crate
27    /// (Rust crate name or Cargo package name, e.g. `std`, `core`, `my-crate`).
28    /// Useful for standard-library workspaces and sub-workspaces.
29    #[arg(long = "crate")]
30    pub crate_name: Option<String>,
31    /// Filter verification targets to only those within the specified module path
32    /// (e.g. `my_module::inner`). When combined with `--crate`, the path is
33    /// interpreted relative to that crate. Applies to all verification modes.
34    #[arg(long)]
35    pub module: Option<String>,
36}
rapx/cli/verify.rs

rapx/cli/
verify.rs
