1 files changed, 37 insertions, 13 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 2b9a54a4..4cb4ded6 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -199,6 +199,10 @@ let builtins_generic = {
         (TFloat(FDouble, []),
           [TPtr(TVoid [], [])],
           false);
+    "__compcert_va_composite",
+        (TPtr(TVoid [], []),
+          [TPtr(TVoid [], []); TInt(IUInt, [])],
+          false);
   (* Helper functions for int64 arithmetic *)
     "__i64_dtos",
         (TInt(ILongLong, []),
@@ -381,26 +385,46 @@ let va_list_ptr e =
     | Evalof(e', _) -> Eaddrof(e', Tpointer(typeof e, noattr))
     | _             -> error "bad use of a va_list object"; e
 
-let make_builtin_va_arg env ty e =
-  let (helper, ty_ret) =
-    match ty with
-    | Tint _ | Tpointer _ ->
-        ("__compcert_va_int32", Tint(I32, Unsigned, noattr))
-    | Tlong _ ->
-        ("__compcert_va_int64", Tlong(Unsigned, noattr))
-    | Tfloat _ ->
-        ("__compcert_va_float64", Tfloat(F64, noattr))
-    | _ ->
-        unsupported "va_arg at this type";
-        ("", Tvoid) in
+let make_builtin_va_arg_by_val helper ty ty_ret arg =
   let ty_fun =
     Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, cc_default) in
   Ecast 
     (Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun),
-           Econs(va_list_ptr e, Enil),
+           Econs(va_list_ptr arg, Enil),
            ty_ret),
      ty)
 
+let make_builtin_va_arg_by_ref helper ty arg =
+  let ty_fun =
+    Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), 
+              Tpointer(Tvoid, noattr), cc_default) in
+  let ty_ptr =
+    Tpointer(ty, noattr) in
+  let call =
+    Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun),
+          Econs(va_list_ptr arg, 
+                Econs(Esizeof(ty, Tint(I32, Unsigned, noattr)), Enil)),
+          Tpointer(Tvoid, noattr)) in
+  Evalof(Ederef(Ecast(call, ty_ptr), ty), ty)
+
+let make_builtin_va_arg env ty e =
+  match ty with
+  | Tint _ | Tpointer _ ->
+      make_builtin_va_arg_by_val 
+        "__compcert_va_int32" ty (Tint(I32, Unsigned, noattr)) e
+  | Tlong _ ->
+      make_builtin_va_arg_by_val 
+        "__compcert_va_int64" ty (Tlong(Unsigned, noattr)) e
+  | Tfloat _ ->
+      make_builtin_va_arg_by_val 
+        "__compcert_va_float64" ty (Tfloat(F64, noattr)) e
+  | Tstruct _ | Tunion _ ->
+      make_builtin_va_arg_by_ref
+        "__compcert_va_composite" ty e
+  | _ ->
+      unsupported "va_arg at this type";
+      Eval(Vint(coqint_of_camlint 0l), type_int32s)
+
 (** ** Translation functions *)
 
 (** Constants *)