diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-11-10 10:02:07 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-11-12 09:58:30 +0100 |
| commit | 6431b483760b6b039f97a1749a055a3c181084b4 (patch) | |
| tree | c635aaf636150d2b89366e5e0e138b56b1b612a6 /cfrontend | |
| parent | d194e47a7d494944385ff61c194693f8a67787cb (diff) | |
| download | compcert-kvx-6431b483760b6b039f97a1749a055a3c181084b4.tar.gz compcert-kvx-6431b483760b6b039f97a1749a055a3c181084b4.zip | |
Resurrect a warning for bit fields of enum types
Earlier CompCert versions would warn if a bit field of width N and
type enum E was too small for the values of the enumeration: whether
the field is interpreted as a N-bit signed integer or a N-bit unsigned
integer, some values of the enumeration are not representable.
This warning was performed in the Bitfields emulation pass, which went
away during the reimplementation of bit fields within the verified
part of CompCert.
In this commit, we resurrect the warning and perform it during the Elab pass.
In passing, some of the code that elaborates bit fields was moved to a
separate function "check_bitfield".
Diffstat (limited to 'cfrontend')
0 files changed, 0 insertions, 0 deletions