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/Op.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/Op.v')
-rw-r--r-- | ia32/Op.v | 9 |
1 files changed, 5 insertions, 4 deletions
@@ -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 |