From 4297fcb821c3188449b64184af73e41491a6118f Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 23 Jul 2012 15:01:54 +0000
Subject: - Revised non-overflow constraints on memory injections so that  
 injections compose (Values, Memdata, Memory) - Memory chunks: Mfloat64 now
 has alignment 8; introduced Mfloat64al32   that works like old Mfloat64 (i.e.
 has alignment 4); simplified   handling of memcpy builtin accordingly.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1983 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/SelectOp.vp | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'arm/SelectOp.vp')

diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 6049017c..9296ce62 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -426,6 +426,7 @@ Definition can_use_Aindexed2 (chunk: memory_chunk): bool :=
   | Mint32 => true
   | Mfloat32 => false
   | Mfloat64 => false
+  | Mfloat64al32 => false
   end.
 
 Definition can_use_Aindexed2shift (chunk: memory_chunk): bool :=
@@ -437,6 +438,7 @@ Definition can_use_Aindexed2shift (chunk: memory_chunk): bool :=
   | Mint32 => true
   | Mfloat32 => false
   | Mfloat64 => false
+  | Mfloat64al32 => false
   end.
 
 Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
-- 
cgit