Struct ArmSemantics 

pub struct ArmSemantics;

ARM semantics encoder

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

Implementations

impl ArmSemantics

pub fn new() -> Self

Create a new ARM semantics encoder

pub fn encode_op(&self, op: &ArmOp, state: &mut ArmState)

Encode an ARM operation and return the resulting state

This models the effect of executing the ARM instruction on the processor state.

pub fn extract_result(&self, state: &ArmState, reg: &Reg) -> BV

Extract the result value from a register after execution

Trait Implementations

impl Default for ArmSemantics

fn default() -> Self

Returns the “default value” for a type.