aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/C2C.ml
diff options
context:
space:
mode:
authorMichael Schmidt <github@mschmidt.me>2016-11-07 13:34:56 +0100
committerMichael Schmidt <github@mschmidt.me>2016-11-07 13:34:56 +0100
commit55edd9487813518d67566002d88cc7394cc0c61a (patch)
tree1486f78d22f4f263f6a8a95e13e927fa47c579a1 /cfrontend/C2C.ml
parenta8f87aa382b192c6392cb506ca204599fe7fd86a (diff)
downloadcompcert-55edd9487813518d67566002d88cc7394cc0c61a.tar.gz
compcert-55edd9487813518d67566002d88cc7394cc0c61a.zip
extend constant check for builtin_memcpy_aligned (bug 20320)
Diffstat (limited to 'cfrontend/C2C.ml')
-rw-r--r--cfrontend/C2C.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index a1ca48d1..43a18a52 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -365,10 +365,12 @@ let make_builtin_memcpy args =
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
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.Int.is_power2 al1 = None then
error "alignment argument of '__builtin_memcpy_aligned' must be a power of 2";