From 59646439baa1b9cc6209b684e4ccf9aac908fdbc Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 17 Apr 2010 07:01:18 +0000
Subject: Support __builtin_memcpy; use it for struct assignment

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1319 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/C2Clight.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'cfrontend')

diff --git a/cfrontend/C2Clight.ml b/cfrontend/C2Clight.ml
index 100c72b1..614ad770 100644
--- a/cfrontend/C2Clight.ml
+++ b/cfrontend/C2Clight.ml
@@ -841,6 +841,19 @@ let builtins_generic = {
          (TVoid [], [TPtr(TVoid [], []); TFloat(FDouble, [])], false);
     "__builtin_volatile_write_pointer",
          (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false)
+    (* Block copy *)
+    "__builtin_memcpy",
+         (TPtr(TVoid [], []),
+           [TPtr(TVoid [], []); 
+            TPtr(TVoid [AConst], []); 
+            TInt(Cutil.size_t_ikind, [])],
+          false);
+    "__builtin_memcpy_words",
+         (TPtr(TVoid [], []),
+           [TPtr(TVoid [], []); 
+            TPtr(TVoid [AConst], []); 
+            TInt(Cutil.size_t_ikind, [])],
+          false)
   ]
 }
 
-- 
cgit