diff options
| author | Michael Schmidt <github@mschmidt.me> | 2016-11-08 15:53:31 +0100 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2016-11-08 15:53:31 +0100 |
| commit | 363a47b6b77f69d8f2a074b395b5183197d61c0c (patch) | |
| tree | 69810543444155a07f4eb8b3156d435e7caa4cdf /cfrontend/C2C.ml | |
| parent | 6679544e5018695bbdf5f726b0c36f89a92412f5 (diff) | |
| download | compcert-kvx-363a47b6b77f69d8f2a074b395b5183197d61c0c.tar.gz compcert-kvx-363a47b6b77f69d8f2a074b395b5183197d61c0c.zip | |
fix va_arg for pointer types on 64bit target
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 1dbbc775..c0c62daa 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -415,9 +415,15 @@ let make_builtin_va_arg_by_ref helper ty arg = let make_builtin_va_arg env ty e = match ty with - | Ctypes.Tint _ | Tpointer _ -> + | Ctypes.Tint _ -> make_builtin_va_arg_by_val "__compcert_va_int32" ty (Tint(I32, Unsigned, noattr)) e + | Tpointer _ when Archi.ptr64 = false -> + make_builtin_va_arg_by_val + "__compcert_va_int32" ty (Tint(I32, Unsigned, noattr)) e + | Tpointer _ when Archi.ptr64 = true -> + make_builtin_va_arg_by_val + "__compcert_va_int64" ty (Tlong(Unsigned, noattr)) e | Tlong _ -> make_builtin_va_arg_by_val "__compcert_va_int64" ty (Tlong(Unsigned, noattr)) e |