Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Improve portability of the test for annotations inclightgen | Xavier Leroy | 2020-06-05 | 1 | -0/+2 |
| | | | | __builtin_ais_annot is not supported for macOS nor for Cygwin. | ||||
* | clightgen: fix the printing of annotations | Xavier Leroy | 2020-06-05 | 1 | -0/+6 |
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 |