Lines Matching defs:addr
101 val addr = dest_address (subst i ``a:word64``)
103 in GUARD_EQUAL_BYTE (addr,imm) end
130 val addr = dest_address (subst i ``a:word64``)
131 in (ACCESS_WORD,addr) end handle HOL_ERR _ => fail()
134 val addr = dest_address (subst i ``a:word64``)
135 in (ACCESS_BYTE,addr) end handle HOL_ERR _ => fail()
147 val addr = dest_address (subst i ``a:word64``)
151 in (ACCESS_WORD,addr,x) end handle HOL_ERR _ => let
153 val addr = dest_address (subst i ``a:word64``)
156 in (ACCESS_WORD,addr,ASSIGN_X_CONST x) end