diff options
Diffstat (limited to 'ia32/CBuiltins.ml')
| -rw-r--r-- | ia32/CBuiltins.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml index cbd5998c..b594c65e 100644 --- a/ia32/CBuiltins.ml +++ b/ia32/CBuiltins.ml @@ -18,7 +18,9 @@ open C let builtins = { - Builtins.typedefs = []; + Builtins.typedefs = [ + "__builtin_va_list", TPtr(TVoid [], []) + ]; Builtins.functions = [ (* Integer arithmetic *) "__builtin_bswap", @@ -45,3 +47,5 @@ let builtins = { (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false); ] } + +let size_va_list = 4 |