diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-06-05 16:43:43 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-06-05 16:52:45 +0200 |
| commit | 8f750f2d4d68192d92b6363490e8a8e577f55584 (patch) | |
| tree | b6829877eb75dfdf0d82e1684bbe0da0a5583c72 /cfrontend | |
| parent | 08491de0566dbd8cfe7a9cd4ca129a5a05caf196 (diff) | |
| download | compcert-8f750f2d4d68192d92b6363490e8a8e577f55584.tar.gz compcert-8f750f2d4d68192d92b6363490e8a8e577f55584.zip | |
clightgen: fix the printing of annotations
The printing of EF_annot and EF_annot_val was missing the extra "kind"
parameter introduced in commit 6a010b4.
Also: the automatic translation of annotations into Coq assertions
was confusing and prevented other uses of __builtin_annot statements
in conjunction with clightgen. I believe it was never used.
This commit removes this translation.
Closes: #360
Diffstat (limited to 'cfrontend')
0 files changed, 0 insertions, 0 deletions