Struct WasmSemantics 

pub struct WasmSemantics { /* private fields */ }

WASM semantics encoder

Z3 0.19 uses thread-local context – no lifetime parameters needed.

Implementations

impl WasmSemantics

pub fn new() -> Self

Create a new WASM semantics encoder

pub fn new_with_memory(memory: Vec<BV>) -> Self

Create encoder with mutable memory for load/store operations

pub fn encode_op(&self, op: &WasmOp, inputs: &[BV]) -> BV

Encode a WASM operation as an SMT formula

Returns a bitvector representing the result of the operation. For operations with multiple operands, inputs are provided as a slice.

Trait Implementations

impl Default for WasmSemantics

fn default() -> Self

Returns the “default value” for a type.