From 48b839d15e69c3c9995ca3c25e6a7c4730224292 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 13 Jul 2012 15:01:51 +0000 Subject: 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 --- ia32/Asm.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'ia32/Asm.v') diff --git a/ia32/Asm.v b/ia32/Asm.v index e2176fdc..a6a03ed4 100644 --- a/ia32/Asm.v +++ b/ia32/Asm.v @@ -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 => -- cgit