diff options
| -rw-r--r-- | cfrontend/C2C.ml | 28 | ||||
| -rw-r--r-- | lib/Camlcoq.ml | 6 |
2 files changed, 22 insertions, 12 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 7ba39be4..439cc584 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -143,8 +143,8 @@ let builtins_generic = { (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [AConst], []); - TInt(IUInt, []); - TInt(IUInt, [])], + TInt(IULong, []); + TInt(IULong, [])], false); (* Annotations *) "__builtin_annot", @@ -359,22 +359,26 @@ let globals_for_strings globs = (** ** Handling of inlined memcpy functions *) +let constant_size_t a = + match Initializers.constval_cast !comp_env a Ctyping.size_t with + | Errors.OK(Vint n) -> Some(Integers.Int.unsigned n) + | Errors.OK(Vlong n) -> Some(Integers.Int64.unsigned n) + | _ -> None + let make_builtin_memcpy args = match args with | Econs(dst, Econs(src, Econs(sz, Econs(al, Enil)))) -> let sz1 = - match Initializers.constval !comp_env sz with - | Errors.OK(Vint n) -> n - | Errors.OK(Vlong n) -> n - | _ -> error "size argument of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.zero in + match constant_size_t sz with + | Some n -> n + | None -> error "size argument of '__builtin_memcpy_aligned' must be a constant"; Z.zero in let al1 = - match Initializers.constval !comp_env al with - | 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.Int64.is_power2 al1 = None then + match constant_size_t al with + | Some n -> n + | None -> error "alignment argument of '__builtin_memcpy_aligned' must be a constant"; Z.one in + if not (Z.is_power2 al1) then error "alignment argument of '__builtin_memcpy_aligned' must be a power of 2"; - if Integers.Int64.modu sz1 al1 <> Integers.Int.zero then + if not (Z.eq (Z.modulo sz1 al1) Z.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), diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index 5b5d37ee..63a31181 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -170,6 +170,8 @@ module Z = struct let add = Z.add let sub = Z.sub let mul = Z.mul + let div = Z.div + let modulo = Z.modulo let eq x y = (Z.compare x y = Eq) let lt x y = (Z.compare x y = Lt) let gt x y = (Z.compare x y = Gt) @@ -247,9 +249,13 @@ module Z = struct let to_string = dec + let is_power2 x = + gt x zero && eq (Z.coq_land x (pred x)) zero + let (+) = add let (-) = sub let ( * ) = mul + let ( / ) = div let (=) = eq let (<) = lt let (<=) = le |