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
---
 checklink/Check.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'checklink/Check.ml')

diff --git a/checklink/Check.ml b/checklink/Check.ml
index c60a4a7..d1b6007 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -2420,7 +2420,7 @@ and check_builtin_vload_common ccode ecode pc chunk addr offset res fw =
           >>= recur_simpl
       | _ -> error
       end
-  | Mfloat64, FR res ->
+  | (Mfloat64 | Mfloat64al32), FR res ->
       begin match ecode with
       | LFD(frD, rA, d) :: es ->
           OK(fw)
@@ -2480,7 +2480,7 @@ and check_builtin_vstore_common ccode ecode pc chunk addr offset src fw =
           >>= compare_code ccode es (Int32.add pc 8l)
       | _ -> error
       end
-  | Mfloat64, FR src ->
+  | (Mfloat64 | Mfloat64al32), FR src ->
       begin match ecode with
       | STFD(frS, rA, d) :: es ->
           OK(fw)
-- 
cgit v1.2.3