diff options
author | Michael Schmidt <github@mschmidt.me> | 2016-11-07 13:34:56 +0100 |
---|---|---|
committer | Michael Schmidt <github@mschmidt.me> | 2016-11-07 13:34:56 +0100 |
commit | 55edd9487813518d67566002d88cc7394cc0c61a (patch) | |
tree | 1486f78d22f4f263f6a8a95e13e927fa47c579a1 /cfrontend | |
parent | a8f87aa382b192c6392cb506ca204599fe7fd86a (diff) | |
download | compcert-55edd9487813518d67566002d88cc7394cc0c61a.tar.gz compcert-55edd9487813518d67566002d88cc7394cc0c61a.zip |
extend constant check for builtin_memcpy_aligned (bug 20320)
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/C2C.ml | 2 |
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"; |