Skip to main content

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}