| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
| |
As proposed in #404.
This is presented as a new option `-clight` to the existing `clightgen` tool.
Revise clightgen testing to test the Csyntax output in addition to
the Clight output.
|
|
|
|
|
|
|
| |
Split reusable parts of ExportClight.ml off, into
ExportBase.ml and ExportCtypes.ml.
Rename exportclight/ directory to export/
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 `_`.
|
|
|
|
|
| |
The configure script still accepts "macosx" for backward compatibility,
but every other part of CompCert now uses "macos".
|
| |
|
|
|
|
| |
Use different combination of options for different test files.
|
|
|
|
| |
configure flags -use-external-Flocq and -use external-MenhirLib.
|
|
|
|
| |
__builtin_ais_annot is not supported for macOS nor for Cygwin.
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
| |
A "dollar" sign in a function name or a global variable name was producing
incorrect Coq identifiers. (Issue #319.)
|
| |
|
|
|
|
|
| |
It's not really necessary, and under Windows it's really ../../clightgen.exe,
which confuses make.
|
|
Also: add "parallel" entry to test/Makefile for parallel execution of tests.
|