summaryrefslogtreecommitdiff
path: root/ia32/Asmgen.v
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-07-13 15:01:51 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-07-13 15:01:51 +0000
commit48b839d15e69c3c9995ca3c25e6a7c4730224292 (patch)
tree2394d10bcb90b36617bfd79f32aa5e04492a860a /ia32/Asmgen.v
parent926bf226e89e0a4935da8815852af76c8d2b3cdf (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/Asmgen.v')
-rw-r--r--ia32/Asmgen.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index 478cdf5..5603d85 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -322,6 +322,9 @@ Definition transl_op
| Ofloatconst f, nil =>
do r <- freg_of res;
OK ((if Float.eq_dec f Float.zero then Pxorpd_f r else Pmovsd_fi r f) :: k)
+ | Oaddrsymbol id, nil =>
+ do r <- ireg_of res;
+ OK (Pmov_raddr r id :: k)
| Ocast8signed, a1 :: nil =>
do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovsb_rr r r1 k
| Ocast8unsigned, a1 :: nil =>