aboutsummaryrefslogtreecommitdiffstats
path: root/x86/CBuiltins.ml
diff options
context:
space:
mode:
Diffstat (limited to 'x86/CBuiltins.ml')
-rw-r--r--x86/CBuiltins.ml8
1 files changed, 6 insertions, 2 deletions
diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml
index 6820c089..a16f3ef7 100644
--- a/x86/CBuiltins.ml
+++ b/x86/CBuiltins.ml
@@ -19,8 +19,12 @@ open C
let (va_list_type, va_list_scalar, size_va_list) =
if Archi.ptr64 then
- (* Actually a struct passed by reference; equivalent to 3 64-bit words *)
- (TArray(TInt(IULong, []), Some 3L, []), false, 3*8)
+ if Archi.win64 then
+ (* Just a pointer *)
+ (TPtr(TVoid [], []), true, 8)
+ else
+ (* Actually a struct passed by reference; equivalent to 3 64-bit words *)
+ (TArray(TInt(IULong, []), Some 3L, []), false, 3*8)
else
(* Just a pointer *)
(TPtr(TVoid [], []), true, 4)