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 --- ia32/CBuiltins.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'ia32/CBuiltins.ml') 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 -- cgit v1.2.3