diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-05-19 11:08:22 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-05-19 11:08:22 +0200 |
| commit | 318fc06823eb577e9b386aeea57133e8c3938ecf (patch) | |
| tree | 1c03ea0eb7061bc72d616fc917e1c6450e28990b /aarch64/Asm.v | |
| parent | 413bd7681ed70155b7bbc9ab2255801ed41904ea (diff) | |
| download | compcert-318fc06823eb577e9b386aeea57133e8c3938ecf.tar.gz compcert-318fc06823eb577e9b386aeea57133e8c3938ecf.zip | |
Improve control-flow analysis of "noreturn" function calls
- Honor "noreturn" attributes and _Noreturn declarations on calls to
function pointers.
- Don't crash if a function type is an unknown typedef.
(This can happen with local typedefs.)
Instead, conservatively assume this function can return.
Diffstat (limited to 'aarch64/Asm.v')
0 files changed, 0 insertions, 0 deletions