Struct FactSpecResult 

pub struct FactSpecResult {
    pub ops: Vec<WasmOp>,
    pub block_arity: Vec<(u8, u8)>,
    pub kept: Vec<usize>,
    pub admitted: Vec<String>,
    pub declined: Vec<String>,
    pub elide_div_zero: Vec<usize>,
    pub elide_div_ovf: Vec<usize>,
    /* private fields */
}

Outcome of specializing one function. ops/block_arity/kept are only meaningful when changed — otherwise they echo the input.

Fields

ops: Vec<WasmOp>

The (possibly rewritten) op stream.

block_arity: Vec<(u8, u8)>

The blocktype-arity side-table matching ops (one entry per Block/Loop/If in op order — entries of deleted openers removed).

kept: Vec<usize>

Indices into the ORIGINAL op stream that were kept, in order. Lets the driver filter parallel side-tables (e.g. op_offsets for DWARF).

admitted: Vec<String>

One certificate line per ADMITTED elision (logged per function).

declined: Vec<String>

One line per LOUD DECLINE (the general lowering is emitted for these).

elide_div_zero: Vec<usize>

#494 phase 2b: indices (into the RETURNED ops stream) of div/rem ops whose divide-by-zero trap guard was certificate-elided (UNSAT(P ∧ divisor == 0) discharged per site).

elide_div_ovf: Vec<usize>

#494 phase 2b: indices (into the RETURNED ops stream) of div_s ops whose INT_MIN / -1 overflow guard was certificate-elided — a SEPARATE obligation (UNSAT(P ∧ dividend == INT_MIN ∧ divisor == -1)); a divisor-nonzero fact alone never lands here (#633/#634).

Implementations

impl FactSpecResult

pub fn changed(&self) -> bool

True when the op STREAM was rewritten (region deletions). Guard-elision marks do not rewrite the stream — check elide_div_zero / elide_div_ovf separately.

Trait Implementations

impl Debug for FactSpecResult

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

Formats the value using the given formatter.