diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-08 11:42:39 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-08 11:42:39 +0200 |
commit | f869da75c970aec78975f7154c806f29e3012b7a (patch) | |
tree | 32bd1fc3fc05e51d7d339956b04196f80e0f2116 /cparser/Elab.ml | |
parent | 3eb2b3b7bb464d9844f7c161fbcff53f597348b9 (diff) | |
download | compcert-f869da75c970aec78975f7154c806f29e3012b7a.tar.gz compcert-f869da75c970aec78975f7154c806f29e3012b7a.zip |
Turn off copy optimization when returning a composite by reference.
The copy optimization is not correct in case of overlap between destination
and source. We would need to use an hypothetical __builtin_memmove_aligned
that can cope with overlap to implement the copy at return of callee.
Diffstat (limited to 'cparser/Elab.ml')
0 files changed, 0 insertions, 0 deletions