diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-01-01 17:25:27 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-01-01 17:25:27 +0000 |
| commit | c5ca995063b270c0e0b0f4df04c68ae431c869fd (patch) | |
| tree | 7dd6ddb03a667e00c03be86b158741e3eb175348 | |
| parent | 7e4e9417b6bfaf9f6a0f36e2fc040c12f8530889 (diff) | |
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
| -rw-r--r-- | arm/CBuiltins.ml | 1 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 13 | ||||
| -rw-r--r-- | ia32/CBuiltins.ml | 1 | ||||
| -rw-r--r-- | powerpc/CBuiltins.ml | 1 | ||||
| -rw-r--r-- | runtime/powerpc/vararg.s | 6 |
5 files changed, 15 insertions, 7 deletions
diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml index a8583c8..b9b54e4 100644 --- a/arm/CBuiltins.ml +++ b/arm/CBuiltins.ml @@ -47,3 +47,4 @@ let builtins = { } let size_va_list = 4 +let va_list_scalar = true 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) diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml index b594c65..6dbabf1 100644 --- a/ia32/CBuiltins.ml +++ b/ia32/CBuiltins.ml @@ -49,3 +49,4 @@ let builtins = { } let size_va_list = 4 +let va_list_scalar = true diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 8405c4f..db01ae1 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -89,3 +89,4 @@ let builtins = { } let size_va_list = 12 +let va_list_scalar = false diff --git a/runtime/powerpc/vararg.s b/runtime/powerpc/vararg.s index 98de6c8..2b36d61 100644 --- a/runtime/powerpc/vararg.s +++ b/runtime/powerpc/vararg.s @@ -44,9 +44,9 @@ # } * regs; // pointer to saved register area # } va_list[1]; # -# unsigned int __compcert_va_int32(va_list * ap); -# unsigned long long __compcert_va_int64(va_list * ap); -# double __compcert_va_float64(va_list * ap); +# unsigned int __compcert_va_int32(va_list ap); +# unsigned long long __compcert_va_int64(va_list ap); +# double __compcert_va_float64(va_list ap); .text |