diff options
| author | Michael Schmidt <github@mschmidt.me> | 2016-11-07 14:09:16 +0100 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2016-11-07 14:09:16 +0100 |
| commit | 6679544e5018695bbdf5f726b0c36f89a92412f5 (patch) | |
| tree | b64a6fcd69b7b305c8c8abfa67ba9c2d634ff1d3 /cfrontend | |
| parent | 55edd9487813518d67566002d88cc7394cc0c61a (diff) | |
| download | compcert-kvx-6679544e5018695bbdf5f726b0c36f89a92412f5.tar.gz compcert-kvx-6679544e5018695bbdf5f726b0c36f89a92412f5.zip | |
extend constant check for builtin_memcpy_aligned (bug 20320)
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/C2C.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 43a18a52..1dbbc775 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), |