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: &VerificationScope) -> bool

This method tests for !=.

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 StructuralPartialEq for VerificationScope