aboutsummaryrefslogtreecommitdiffstats
path: root/common/AST.v
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-01-12 10:48:56 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-01-12 10:48:56 +0000
commit7998ccfd709b97f1a2306df4570365d58a5bb4b5 (patch)
treebf76efed90d88ede9e44187072b9cbd5265aab66 /common/AST.v
parent362f2f36a44fa6ab4fe28264ed572d721adece70 (diff)
downloadcompcert-kvx-7998ccfd709b97f1a2306df4570365d58a5bb4b5.tar.gz
compcert-kvx-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.v7
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.