Struct ArmState 

pub struct ArmState {
    pub registers: Vec<BV>,
    pub flags: ConditionFlags,
    pub vfp_registers: Vec<BV>,
    pub memory: Vec<BV>,
    pub locals: Vec<BV>,
    pub globals: Vec<BV>,
    pub may_trap: Bool,
}

ARM processor state representation in SMT

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

Fields

registers: Vec<BV>

General purpose registers R0-R15

flags: ConditionFlags

Condition flags (N, Z, C, V)

vfp_registers: Vec<BV>

VFP (floating-point) registers

memory: Vec<BV>

Memory model (simplified for bounded verification)

locals: Vec<BV>

Local variables (for WASM verification)

globals: Vec<BV>

Global variables (for WASM verification)

may_trap: Bool

VCR-VER-002 (#166): the accumulated condition under which the executed sequence TRAPS (reaches a UDF). false in a fresh state; encode_op sets it unconditionally on a Udf, and the branch-taking executor ArmSemantics::encode_sequence_br conditions it on the path guard the UDF is reached under — this is the ARM-side trap term the trap-preservation VC compares against the WASM op’s trap condition.

Implementations

impl ArmState

pub fn new_symbolic() -> Self

Create a new ARM state with symbolic values

pub fn get_reg(&self, reg: &Reg) -> &BV

Get register value

pub fn set_reg(&mut self, reg: &Reg, value: BV)

Set register value

pub fn get_vfp_reg(&self, reg: &VfpReg) -> &BV

Get VFP register value

pub fn set_vfp_reg(&mut self, reg: &VfpReg, value: BV)

Set VFP register value