Struct AssertionResult 

pub struct AssertionResult {
    pub query: String,
    pub parsed: bool,
    pub now: Option<bool>,
    pub now_detail: String,
    pub verdict: ProofVerdict,
    pub verdict_detail: String,
}

The result of asserting a predicate at the cursor — the dual lens the debugger is built for: what is true now (concrete, from live values) and what is proven for every run (from the Oracle’s static facts, kernel-style interval entailment, no Z3). now is None when a term has no live integer value; the verdict is Unknown when a term has no proven range.

Fields

query: String

parsed: bool

Whether the predicate parsed as a comparison (a < b, x >= 0, …).

now: Option<bool>

Concrete truth at the current state (None if a term isn’t a live integer).

now_detail: String

verdict: ProofVerdict

Static guarantee over every run.

verdict_detail: String

Trait Implementations

impl Clone for AssertionResult

fn clone(&self) -> AssertionResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Serialize for AssertionResult

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

where __S: Serializer,

Serialize this value into the given Serde serializer.