Trait SafetyProperty

pub trait SafetyProperty {
    type Args: SafetyPropertyArg;

    // Required methods
    fn name() -> &'static str;
    fn description(args: Self::Args) -> String;

    // Provided method
    fn kani(args: Self::Args) -> Option<String> { ... }
}

Required Associated Types

type Args: SafetyPropertyArg

A tuple of SP arguments.

Required Methods

fn name() -> &'static str

Single ident name of an SP.

fn description(args: Self::Args) -> String

Static string, or dynamic interpolated string based on tag arguments.

Provided Methods

fn kani(args: Self::Args) -> Option<String>

Kani macros for the SP.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors