| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
|
|
|
| |
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.
|