Struct ExecutionResult 

pub struct ExecutionResult {
    pub plan: InvocationPlan,
    pub status: ExecutionStatus,
    pub stdout: String,
    pub stderr: String,
    pub exit_code: Option<i32>,
    pub backend_version: Option<String>,
    pub smt_output: Option<SmtOutput>,
    pub lean_output: Option<LeanOutput>,
}

Result captured from a verifier invocation.

Fields

plan: InvocationPlan

status: ExecutionStatus

stdout: String

stderr: String

exit_code: Option<i32>

backend_version: Option<String>

smt_output: Option<SmtOutput>

lean_output: Option<LeanOutput>

Implementations

impl ExecutionResult

pub fn verification_policy(&self) -> VerificationPolicy

pub fn is_success(&self) -> bool

pub fn certificate_for_obligation( &self, obligation: &str, ) -> Option<Certificate>

Trait Implementations

impl Clone for ExecutionResult

fn clone(&self) -> ExecutionResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ExecutionResult

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

Formats the value using the given formatter.

impl PartialEq for ExecutionResult

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

Tests for self and other values to be equal, and is used by ==.

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

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

impl Eq for ExecutionResult

impl StructuralPartialEq for ExecutionResult