diff options
author | 2012-07-13 15:01:51 +0000 | |
---|---|---|
committer | 2012-07-13 15:01:51 +0000 | |
commit | 48b839d15e69c3c9995ca3c25e6a7c4730224292 (patch) | |
tree | 2394d10bcb90b36617bfd79f32aa5e04492a860a /ia32/Asm.v | |
parent | 926bf226e89e0a4935da8815852af76c8d2b3cdf (diff) |
Support for MacOS X's indirect symbols. (first try)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1978 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/Asm.v')
-rw-r--r-- | ia32/Asm.v | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -108,6 +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_rm (rd: ireg) (a: addrmode) | Pmov_mr (a: addrmode) (rs: ireg) | Pmovd_fr (rd: freg) (r1: ireg) (**r [movd] (32-bit int) *) @@ -458,6 +459,8 @@ 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 => + Next (nextinstr_nf (rs#rd <- (symbol_offset id Int.zero))) m | Pmov_rm rd a => exec_load Mint32 m a rs rd | Pmov_mr a r1 => |