- 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

1 files changed, 2 insertions, 2 deletions

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)