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>,
}

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)

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