From c5ca995063b270c0e0b0f4df04c68ae431c869fd Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 1 Jan 2014 17:25:27 +0000 Subject: Fine hair splitting depending on whether va_list is a scalar type (IA32, ARM) or an array type (PowerPC). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2395 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/C2C.ml | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 5f99e48..ff4b6c1 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -199,7 +199,10 @@ a constant)"; Integers.Int.one in (** ** Translation of [va_arg] for variadic functions. *) -let eaddrof e = Eaddrof(e, Tpointer(typeof e, noattr)) +let va_list_ptr e = + if CBuiltins.va_list_scalar + then Eaddrof(e, Tpointer(typeof e, noattr)) + else e let make_builtin_va_arg env ty e = let (helper, ty_ret) = @@ -218,7 +221,7 @@ let make_builtin_va_arg env ty e = (Ecall(Evar (intern_string helper, Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, cc_default)), - Econs(eaddrof e, Enil), + Econs(va_list_ptr e, Enil), ty_ret), ty) @@ -613,7 +616,9 @@ let rec convertExpr env e = Eunop(Oabsfloat, convertExpr env arg, ty) | C.ECall({edesc = C.EVar {name = "__builtin_va_start"}} as fn, [arg]) -> - Ecall(convertExpr env fn, Econs(eaddrof(convertExpr env arg), Enil), ty) + Ecall(convertExpr env fn, + Econs(va_list_ptr(convertExpr env arg), Enil), + ty) | C.ECall({edesc = C.EVar {name = "__builtin_va_arg"}}, [arg1; arg2]) -> make_builtin_va_arg env ty (convertExpr env arg1) @@ -627,7 +632,7 @@ let rec convertExpr env e = Ebuiltin(EF_memcpy(Z.of_uint CBuiltins.size_va_list, Z.of_uint 4), Tcons(Tpointer(Tvoid, noattr), Tcons(Tpointer(Tvoid, noattr), Tnil)), - Econs(eaddrof dst, Econs(eaddrof src, Enil)), + Econs(va_list_ptr dst, Econs(va_list_ptr src, Enil)), Tvoid) | C.ECall({edesc = C.EVar {name = "printf"}}, args) -- cgit v1.2.3