Lines Matching defs:addr
101 val addr = dest_address (subst i ``a:word32``)
103 in GUARD_EQUAL_BYTE (addr,imm) end
145 val addr = dest_address (subst i ``a:word32``)
149 in (ACCESS_WORD,addr,x) end handle HOL_ERR _ => let
151 val addr = dest_address (subst i ``a:word32``)
155 in (ACCESS_BYTE,addr,x) end handle HOL_ERR _ => let
157 val addr = dest_address (subst i ``a:word32``)
160 in (ACCESS_BYTE,addr,ASSIGN_X_CONST x) end handle HOL_ERR _ => let
162 val addr = dest_address (subst i ``a:word32``)
165 in (ACCESS_WORD,addr,ASSIGN_X_CONST x) end