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

1 files changed, 13 insertions, 0 deletions

diff --git a/cfrontend/C2Clight.ml b/cfrontend/C2Clight.ml
index 100c72b..614ad77 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)
   ]
 }