diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-14 08:05:36 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-14 08:05:36 +0000 |
| commit | bd85aba84475dd956af21c461c44a584958099d1 (patch) | |
| tree | bab1cefe9f84210559a4716a070d79967b60f2b5 /ia32/Asm.v | |
| parent | 48b839d15e69c3c9995ca3c25e6a7c4730224292 (diff) | |
| download | compcert-bd85aba84475dd956af21c461c44a584958099d1.tar.gz compcert-bd85aba84475dd956af21c461c44a584958099d1.zip | |
Support for indirect symbols under MacOS X (final).
Remove stdio hack in runtime/
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1979 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
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 |