Struct VerifyArgs 

pub struct VerifyArgs {
    pub prepare_targets: bool,
    pub postfix_repeat: PostfixRepeat,
    pub mode: VerifyMode,
    pub skip_invariant: bool,
    pub crate_name: Option<String>,
    pub module: Option<String>,
    pub debug_contracts: bool,
}

Arguments for the verify command.

Fields

prepare_targets: bool

Identify all functions annotated with #[rapx::verify] and print each target, its unsafe callees, and their safety contracts.

postfix_repeat: PostfixRepeat

Number of extra SCC postfix repetitions allowed during path enumeration. auto (default): automatic loop-depth detection for InBound and Align. A number ≥ 0 sets a fixed repeat count.

mode: VerifyMode

Verification mode: scan auto-detects unannotated unsafe targets (default), targeted verifies #[rapx::verify] functions.

skip_invariant: bool

Skip struct invariant checks and derive safety via constructor-mutator-method chains. Works with both scan and targeted modes.

crate_name: Option<String>

Filter verification targets to only those within the specified crate (Rust crate name or Cargo package name, e.g. std, core, my-crate). Useful for standard-library workspaces and sub-workspaces.

module: Option<String>

Filter verification targets to only those within the specified module path (e.g. my_module::inner). When combined with --crate, the path is interpreted relative to that crate. Applies to all verification modes.

debug_contracts: bool

Print all contract resolutions for every verification target: each unsafe callee with its resolved contracts, and the caller’s own contracts (expanded form). Useful for debugging missing or unexpected contract resolutions.

Trait Implementations

impl Args for VerifyArgs

fn group_id() -> Option<Id>

Report the [ArgGroup::id][crate::ArgGroup::id] for this set of arguments

fn augment_args<'b>(__clap_app: Command) -> Command

Append to [Command] so it can instantiate Self via [FromArgMatches::from_arg_matches_mut]

fn augment_args_for_update<'b>(__clap_app: Command) -> Command

Append to [Command] so it can instantiate self via [FromArgMatches::update_from_arg_matches_mut]

impl Clone for VerifyArgs

fn clone(&self) -> VerifyArgs

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for VerifyArgs

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl FromArgMatches for VerifyArgs

fn from_arg_matches(__clap_arg_matches: &ArgMatches) -> Result<Self, Error>

Instantiate Self from [ArgMatches], parsing the arguments as needed.

fn from_arg_matches_mut( __clap_arg_matches: &mut ArgMatches, ) -> Result<Self, Error>

Instantiate Self from [ArgMatches], parsing the arguments as needed.

fn update_from_arg_matches( &mut self, __clap_arg_matches: &ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

fn update_from_arg_matches_mut( &mut self, __clap_arg_matches: &mut ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.