diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-11-17 13:40:49 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-11-17 13:48:43 +0100 |
commit | 252a3b44b1cda99344a7554d1d770cabc47a3102 (patch) | |
tree | 09179d0a80fc537c9a1ead0c64ac8646ebd2453a /cparser/StructReturn.ml | |
parent | a3c1aed82d88df7592e63531dc8ce24482da1c28 (diff) | |
download | compcert-252a3b44b1cda99344a7554d1d770cabc47a3102.tar.gz compcert-252a3b44b1cda99344a7554d1d770cabc47a3102.zip |
C2C: revise typing and translation of __builtin_memcpy_aligned
This fixes two issues:
1- The 'size' and 'alignment' arguments of __builtin_memcpy_aligned were declared with type 'unsigned int', which is not good for a 64-bit platform.
2- The corresponding arguments were not cast to type 'unsigned int', causing compilation errors if e.g. the size argument is a 64-bit integer.
(Reported by Michael Schmidt.)
The fix:
1- Evaluate the 3rd and 4th arguments at type size_t
2- Support both Vint and Vlong as results of this evaluation
3- Declare these arguments with type 'unsigned long'.
Supporting work: in lib/Camlcoq.ml, add Z.modulo and Z.is_power2 operations.
Concerning part 3 of the fix, type size_t would be better for future
platforms where size_t is bigger than unsigned long, but some more
work is needed to delay the evaluation of C2C.builtins_generic to
after Cutil.size_t_ikind() is stable, or, equivalently, to evaluate
the cparser/ machine configuration before C2C initializes.
Diffstat (limited to 'cparser/StructReturn.ml')
0 files changed, 0 insertions, 0 deletions