| Commit message (Collapse) | Author | Age | Files | Lines |
|\
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Conflicts:
.gitignore
backend/Lineartyping.v
common/Values.v
configure
cparser/Machine.ml
cparser/Machine.mli
driver/Configuration.ml
driver/Frontend.ml
runtime/Makefile
test/c/Makefile
test/c/aes.c
test/compression/Makefile
test/regression/Makefile
test/regression/extasm.c
test/regression/floats-basics.c
test/regression/floats.c
Note : test/regression should be checked, didn't test it yet
|
| |
| |
| |
| |
| | |
This commit adds a back-end for the AArch64 architecture, namely ARMv8
in 64-bit mode.
|
| | |
|
| | |
|
| | |
|
| | |
|
|\ \
| | |
| | |
| | | |
mppa-work-upstream-merge
|
| |/ |
|
|\|
| |
| |
| | |
mppa-work-upstream-merge
|
| |
| |
| |
| |
| |
| |
| | |
Commit 1df887f breaks compilation on some Windows environments,
those where the output of `menhir --suggest-menhirLib` contains `\r\n` end-of-lines
or backslashes in paths. The fix is to filter the output.
Closes: #304 Changes in configure broke Windows build
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
What's new:
1. A rewrite of the Coq interpreter of Menhir automaton, with
dependent types removing the need for runtime checks for the
well-formedness of the LR stack. This seem to cause some speedup on
the parsing time (~10% for lexing + parsing).
2. Thanks to 1., it is now possible to avoid the use of int31 for
comparing symbols: Since this is only used for validation,
positives are enough.
3. Speedup of Validation: on my machine, the time needed for compiling
Parser.v goes from about 2 minutes to about 1 minute. This seem to
be related to a performance bug in the completeness validator and
to the use of positive instead of int31.
3. Menhir now generates a dedicated inductive type for
(semantic-value-carrying) tokens (in addition to the already
existing inductive type for (non-semantic-value-carrying)
terminals. The end result is that the OCaml support code for the
parser no longer contain calls to Obj.magic. The bad side of this
change is that the formal specification of the parser is perhaps
harder to read.
4. The parser and its library are now free of axioms (I used to use
axiom K and proof irrelevance for easing proofs involving dependent
types).
5. Use of a dedicated custom negative coinductive type for the input
stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a
positive coinductive type, which are now deprecated by Coq.
6. The fuel of the parser is now specified using its logarithm instead
of its actual value. This makes it possible to give large fuel
values instead of using the `let rec fuel = S fuel` hack.
7. Some refactoring in the lexer, the parser and the Cabs syntax tree.
The corresponding changes in Menhir have been released as part of
version 20190626. The `MenhirLib` directory is identical to the
content of the `src` directory of the corresponding `coq-menhirlib`
opam package except that:
- In order to try to make CompCert compatible with several Menhir
versions without updates, we do not check the version of menhir
is compatible with the version of coq-menhirlib. Hence the
`Version.v` file is not present in CompCert's copy.
- Build-system related files have been removed.
|
| | |
|
|\ \ |
|
| |\|
| | |
| | |
| | | |
mppa-if-conversion
|
| | |
| | |
| | |
| | | |
It works fine with the current sources.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Main changes to CompCert outside of Flocq are as follows:
- Minimal supported version of Coq is now 8.7, due to Flocq requirements.
- Most modifications are due to Z2R being dropped in favor of IZR and to
the way Flocq now handles NaNs.
- CompCert now correctly handles NaNs for the Risc-V architecture
(hopefully).
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
As reported in #281, the Menhir packages in Fedora 29 and perhaps in
other distributions can cause `menhir --suggest-menhirLib` to fail
and return an empty path.
This commit detects this situation and aborts configurations.
Also, it hardens the generated Makefile against spaces and special
characters in the path returned by `menhir --suggest-menhirLib`.
|
| | | |
|
| | | |
|
|/ / |
|
| | |
|
| | |
|
| | |
|
| | |
|
|\|
| |
| |
| |
| |
| | |
Conflicts:
.gitignore
runtime/include/stdbool.h
|
| |
| |
| |
| |
| | |
Follow-up to commit fc9bc643. The latest Menhir version compatible
with the current code base is actually 20181113.
|
| |
| |
| | |
The Coq backend of Menhir will soon enjoy a large refactoring, making it incompatible with the version of MenhirLib currently in CompCert. This commit adds a check in configure to make sure that the version of Menhir is not more modern than the current one (20181026).
|
| |
| |
| |
| | |
No other changes are needed to support 8.9.0.
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
J'avais fait une erreur, les __SSE__ c'était quand je compilais sur x86.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
|\|
| |
| |
| |
| | |
Conflicts:
.gitignore
|
| |
| |
| |
| |
| | |
It's not out yet, but based on the state of the v8.8 branch of Coq,
it is very likely to be compatible with CompCert.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The full "usage" text is so long that the actual error message scrolls off
the screen.
With this commit, instead, a short (3-line) error message is printed,
with a suggestion to do `./configure -help`.
The whole "usage" text is printed by `./configure -help`.
Also: better error message for unknown options (arguments starting with `-`).
|
| |
| |
| |
| |
| |
| |
| | |
So that if an error occurs during configuration, there is no
Makefile.config file and "make" will fail.
Closes: #244
|
| | |
|
| |
| |
| |
| | |
Inspired by and adapted from pull request #235 by Benoît Viguier.
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
.vo files are installed if configure options
-install-coqdev or -clightgen or -coqdevdir are given.
Installation directory is $(PREFIX)/lib/compcert/coq by default and
can be changed by configure option -coqdevdir.
Closes: #227
|
| | |
|
| | |
|
| | |
|
| | |
|
|/ |
|