diff options
| -rw-r--r-- | cfrontend/C2C.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 43a18a52..c0c62daa 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -372,9 +372,9 @@ let make_builtin_memcpy args = | Errors.OK(Vint n) -> n | Errors.OK(Vlong n) -> n | _ -> error "alignment argument of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.one in - if Integers.Int.is_power2 al1 = None then + if Integers.Int64.is_power2 al1 = None then error "alignment argument of '__builtin_memcpy_aligned' must be a power of 2"; - if Integers.Int.modu sz1 al1 <> Integers.Int.zero then + if Integers.Int64.modu sz1 al1 <> Integers.Int.zero then error "alignment argument of '__builtin_memcpy_aligned' must be a divisor of the size"; (* Issue #28: must decay array types to pointer types *) Ebuiltin(EF_memcpy(sz1, al1), @@ -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 |