Enum ExecError 

#[non_exhaustive]
pub enum ExecError {
    Incomplete,
    FieldNotFound(String),
    IndexInvalid(u64, String),
    IndexRequired(String),
    SignednessNotEstabilished(String),
    PropertyNotConstructible(String, String),
    InherentPanic,
    InherentPanicDependent,
    NonMonotoneProperty,
    VerifiedInherentAssumed,
    GuiError(String),
    NoResult,
    OtherError(String),
}

Execution error that occured during machine-check execution.

Variants (Non-exhaustive)

Non-exhaustive enums could have additional variants added in future. Therefore, when matching against variants of non-exhaustive enums, an extra wildcard arm must be added to account for any future variants.

Incomplete

The verification result could not be obtained as the abstraction is too coarse.

Currently, this should never happen, as only three-valued abstraction is supported.

FieldNotFound(String)

The specified property field was not found in the system.

IndexInvalid(u64, String)

The used index was invalid.

This can happen either due to the field not being indexable or the index being too high.

IndexRequired(String)

The use of an index is required to use the field in an operation.

This happens because an array type was used where a bit-vector type was expected.

SignednessNotEstabilished(String)

The signedness of the field was required for a comparison, but not estabilished.

Currently, if needed, the signedness must be forced by as_unsigned or as_signed, as field signedness currently does not yet propagate to property verification.

PropertyNotConstructible(String, String)

The specified property is invalid and could not be constructed.

InherentPanic

Verification of a standard property was requested, but the inherent property does not hold.

InherentPanicDependent

Verification of a standard property was requested, but the inherent property is dependent on parameters.

NonMonotoneProperty

Verification of a mu-calculus property encountered a non-monotone change.

This is prohibited as it can lead to infinite verification loops.

VerifiedInherentAssumed

It was requested to verify an inherent property while assuming that it holds.

GuiError(String)

The Graphical User Interface emitted an error.

NoResult

No verification was requested, so there is no verification result.

OtherError(String)

Other error.

Trait Implementations

impl Clone for ExecError

fn clone(&self) -> ExecError

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ExecError

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for ExecError

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Display for ExecError

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

Formats the value using the given formatter.

impl Error for ExecError

fn source(&self) -> Option<&(dyn Error + 'static)>

Returns the lower-level source of this error, if any.

fn description(&self) -> &str

👎Deprecated since 1.42.0: use the Display impl or to_string()

fn cause(&self) -> Option<&dyn Error>

👎Deprecated since 1.33.0: replaced by Error::source, which can support downcasting

fn provide<'a>(&'a self, request: &mut Request<'a>)

🔬This is a nightly-only experimental API. (error_generic_member_access)

Provides type-based access to context intended for error reports.

impl Serialize for ExecError

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

where __S: Serializer,

Serialize this value into the given Serde serializer.