Enum move_model::model::VerificationScope

pub enum VerificationScope {
    Public,
    All,
    Only(String),
    OnlyModule(String),
    None,
}

Verification Scope

Defines what functions to verify.

Variants

Public

Verify only public functions.

All

Verify all functions.

Only(String)

Verify only one function.

OnlyModule(String)

Verify only functions from the given module.

None

Verify no functions

Implementations

impl VerificationScope

pub fn is_exclusive(&self) -> bool

Whether verification is exclusive to only one function or module. If set, this overrides all implicitly included verification targets via invariants and friends.

pub fn get_exclusive_verify_function_name(&self) -> Option<&String>

Returns the target function if verification is exclusive to one function.

Trait Implementations

impl Clone for VerificationScope

fn clone(&self) -> VerificationScope

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for VerificationScope

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

Formats the value using the given formatter.

impl Default for VerificationScope

fn default() -> Self

Returns the “default value” for a type.

impl<'de> Deserialize<'de> for VerificationScope

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq<VerificationScope> for VerificationScope

fn eq(&self, other: &VerificationScope) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for VerificationScope

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for VerificationScope

impl StructuralEq for VerificationScope

impl StructuralPartialEq for VerificationScope