diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-15 10:47:14 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-15 10:47:14 +0200 |
commit | 8eaff6bf3933f2213ae85584009e05123c40fa65 (patch) | |
tree | e15bee84894cb5c4591265b5ed07e9de3e162e54 /cparser/tests/handwritten/dubious-enum.c | |
parent | 4ba1b9e4165cda40e06fca3b563b7561a6cffc70 (diff) | |
download | compcert-8eaff6bf3933f2213ae85584009e05123c40fa65.tar.gz compcert-8eaff6bf3933f2213ae85584009e05123c40fa65.zip |
clightgen: handle empty names given to padding bit fields
In the Clight AST, padding bit fields (such as `int : 6;`) in composite
declarations are given an ident that corresponds to the empty string.
Previously, clightgen would give name `_` to this ident, but this is
not valid Coq.
This commit gives name `empty_ident` to the empty ident. This name
does not start with an underscore, so it cannot conflict with the
names for regular idents, which all start with `_`.
Diffstat (limited to 'cparser/tests/handwritten/dubious-enum.c')
0 files changed, 0 insertions, 0 deletions