From e00261d59ed14721c4b0baab6cd5fe12aeaa06c6 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Tue, 10 Mar 2015 15:18:29 +0100
Subject: Issue #28: if the arguments of __builtin_memcpy_aligned are arrays,
 their types must decay to pointer types in the "types" part of Ebuiltin.

---
 cfrontend/C2C.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 0ccf569b..2b9a54a4 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -365,8 +365,10 @@ a constant)"; Integers.Int.zero in
         | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be 
 a constant)"; Integers.Int.one in
       (* to check: sz1 > 0, al1 divides sz1, al1 = 1|2|4|8 *)
+      (* Issue #28: must decay array types to pointer types *)
       Ebuiltin(EF_memcpy(sz1, al1),
-               Tcons(typeof dst, Tcons(typeof src, Tnil)),
+               Tcons(typeconv(typeof dst),
+                     Tcons(typeconv(typeof src), Tnil)),
                Econs(dst, Econs(src, Enil)), Tvoid)
   | _ ->
     assert false
-- 
cgit