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 /common | |
| parent | 4ba1b9e4165cda40e06fca3b563b7561a6cffc70 (diff) | |
| download | compcert-kvx-8eaff6bf3933f2213ae85584009e05123c40fa65.tar.gz compcert-kvx-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 'common')
0 files changed, 0 insertions, 0 deletions