diff options
Diffstat (limited to 'ia32/Asm.v')
| -rw-r--r-- | ia32/Asm.v | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -108,7 +108,7 @@ Inductive instruction: Type := (** Moves *) | Pmov_rr (rd: ireg) (r1: ireg) (**r [mov] (32-bit int) *) | Pmov_ri (rd: ireg) (n: int) - | Pmov_raddr (rd: ireg) (id: ident) + | Pmov_ra (rd: ireg) (id: ident) | Pmov_rm (rd: ireg) (a: addrmode) | Pmov_mr (a: addrmode) (rs: ireg) | Pmovd_fr (rd: freg) (r1: ireg) (**r [movd] (32-bit int) *) @@ -459,7 +459,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome Next (nextinstr (rs#rd <- (rs r1))) m | Pmov_ri rd n => Next (nextinstr_nf (rs#rd <- (Vint n))) m - | Pmov_raddr rd id => + | Pmov_ra rd id => Next (nextinstr_nf (rs#rd <- (symbol_offset id Int.zero))) m | Pmov_rm rd a => exec_load Mint32 m a rs rd |