From bd85aba84475dd956af21c461c44a584958099d1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 14 Jul 2012 08:05:36 +0000 Subject: 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 --- ia32/Op.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'ia32/Op.v') diff --git a/ia32/Op.v b/ia32/Op.v index a5568c7b..c32de67d 100644 --- a/ia32/Op.v +++ b/ia32/Op.v @@ -69,7 +69,7 @@ Inductive operation : Type := | Omove: operation (**r [rd = r1] *) | Ointconst: int -> operation (**r [rd] is set to the given integer constant *) | Ofloatconst: float -> operation (**r [rd] is set to the given float constant *) - | Oaddrsymbol: ident -> operation (**r [rd] is set to the address of the symbol *) + | Oindirectsymbol: ident -> operation (**r [rd] is set to the address of the symbol *) (*c Integer arithmetic: *) | Ocast8signed: operation (**r [rd] is 8-bit sign extension of [r1] *) | Ocast8unsigned: operation (**r [rd] is 8-bit zero extension of [r1] *) @@ -114,6 +114,7 @@ Inductive operation : Type := (** Derived operators. *) +Definition Oaddrsymbol (id: ident) (ofs: int) : operation := Olea (Aglobal id ofs). Definition Oaddrstack (ofs: int) : operation := Olea (Ainstack ofs). Definition Oaddimm (n: int) : operation := Olea (Aindexed n). @@ -193,7 +194,7 @@ Definition eval_operation | Omove, v1::nil => Some v1 | Ointconst n, nil => Some (Vint n) | Ofloatconst n, nil => Some (Vfloat n) - | Oaddrsymbol id, nil => Some (symbol_address genv id Int.zero) + | Oindirectsymbol id, nil => Some (symbol_address genv id Int.zero) | Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1) | Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1) | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1) @@ -277,7 +278,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Omove => (nil, Tint) (* treated specially *) | Ointconst _ => (nil, Tint) | Ofloatconst _ => (nil, Tfloat) - | Oaddrsymbol _ => (nil, Tint) + | Oindirectsymbol _ => (nil, Tint) | Ocast8signed => (Tint :: nil, Tint) | Ocast8unsigned => (Tint :: nil, Tint) | Ocast16signed => (Tint :: nil, Tint) @@ -542,7 +543,7 @@ Definition two_address_op (op: operation) : bool := | Omove => false | Ointconst _ => false | Ofloatconst _ => false - | Oaddrsymbol _ => false + | Oindirectsymbol _ => false | Ocast8signed => false | Ocast8unsigned => false | Ocast16signed => false -- cgit