| 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/
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
| |
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.
|