diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-01-12 10:48:56 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-01-12 10:48:56 +0000 |
commit | 7998ccfd709b97f1a2306df4570365d58a5bb4b5 (patch) | |
tree | bf76efed90d88ede9e44187072b9cbd5265aab66 /common/AST.v | |
parent | 362f2f36a44fa6ab4fe28264ed572d721adece70 (diff) | |
download | compcert-7998ccfd709b97f1a2306df4570365d58a5bb4b5.tar.gz compcert-7998ccfd709b97f1a2306df4570365d58a5bb4b5.zip |
- Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.
- Revised printing of intermediate RTL code.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common/AST.v')
-rw-r--r-- | common/AST.v | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/common/AST.v b/common/AST.v index 5eee2917..6f35be01 100644 --- a/common/AST.v +++ b/common/AST.v @@ -133,8 +133,7 @@ Inductive memory_chunk : Type := | Mint32 (**r 32-bit integer, or pointer *) | Mint64 (**r 64-bit integer *) | Mfloat32 (**r 32-bit single-precision float *) - | Mfloat64 (**r 64-bit double-precision float *) - | Mfloat64al32. (**r 64-bit double-precision float, 4-aligned *) + | Mfloat64. (**r 64-bit double-precision float *) Definition chunk_eq: forall (c1 c2: memory_chunk), {c1=c2} + {c1<>c2}. Proof. decide equality. Defined. @@ -152,7 +151,6 @@ Definition type_of_chunk (c: memory_chunk) : typ := | Mint64 => Tlong | Mfloat32 => Tsingle | Mfloat64 => Tfloat - | Mfloat64al32 => Tfloat end. Definition type_of_chunk_use (c: memory_chunk) : typ := @@ -165,7 +163,6 @@ Definition type_of_chunk_use (c: memory_chunk) : typ := | Mint64 => Tlong | Mfloat32 => Tfloat | Mfloat64 => Tfloat - | Mfloat64al32 => Tfloat end. (** The chunk that is appropriate to store and reload a value of @@ -174,7 +171,7 @@ Definition type_of_chunk_use (c: memory_chunk) : typ := Definition chunk_of_type (ty: typ) := match ty with | Tint => Mint32 - | Tfloat => Mfloat64al32 + | Tfloat => Mfloat64 | Tlong => Mint64 | Tsingle => Mfloat32 end. |