| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
| |
|
|\
| |
| |
| |
| |
| | |
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
|
| | |
|
| | |
|
| | |
|
| | |
|
|/ |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
| |
When checking for -no-pie and -nopie, evaluate gcc output for error message like 'unknown argument'. (Relying on the error code is not enough.)
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file. OVer the years those two markings got inconsistent.
This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed.
Some build-related files were dual-licensed but some others were not. Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v
Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed. Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST
which is not in lib/
|
|
|
|
| |
It is compatible with 8.7.0 and 8.6.1, no changes required to the Coq sources of CompCert.
|
|
|
|
|
|
| |
configure: accept Coq 8.7.0 and 8.6.1.
(Coq 8.6 became incompatible with commit b4f59c4.)
Changelog: updated.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Clarify that ARMv6 is in fact ARMv6T2
The ARMv6 comes in two flavors depending on the version of the Thumb
instruction set supported: ARMv6 for the original Thumb, ARMv6T2 for Thumb2.
CompCert only supports Thumb2, so its ARMv6 architecture should really be
called ARMv6T2. This makes a difference: the GNU assembler rejects most of
the instructions CompCert generates for ARMv6 with "-mthumb" if the
architecture is specified as ".arch armv6" as opposed to ".arch armv6t2".
This patch fixes the architecture specification in the target printer and
the internal name of the architecture. It does not change the configure
script's flags to avoid breaking changes.
* Always use ARM movw/movt to load large immediates
These move-immediate instructions used to be only emitted in Thumb mode, not
in ARM mode. As far as I understand ARM's documentation, these instructions
are available in *both* modes in ARMv6T2 and above. This should cover all of
CompCert's ARM targets.
Tested for ARMv6 and ARMv7, both with and without Thumb2. The behavior is
now identical to Clang, and the GNU assembler accepts these instructions in
all configurations.
* Separate ARMv6 and ARMv6T2; no movw/movt on ARMv6
- define separate architecture models for ARMv6 and ARMv6T2
- introduce `Archi.move_imm` parameter on ARM to identify models with
`movw`/`movt` move-immediate instructions (all except ARMv6, in both ARM
and Thumb mode)
* Fixes for support for architectures with Thumb2
- rename relevant parameter to `Archi.thumb2_support`
- on ARMv6 without Thumb2, silently accept -marm flag (but not -mthumb)
- allow generation of `sbfx` in ARM mode if Thumb2 is supported
|
|
|
|
| |
Even with __GNUC__ undefined, the standard header files contain bizarre __attribute__ declarations that CompCert fails to parse.
|
| |
|
|\ |
|
| |
| |
| |
| | |
These are the configurations for the new RISC-V port.
|
| |
| |
| |
| | |
8.6.1 works just fine with the current CompCert.
|
|/ |
|
| |
|
| |
|
|
|
|
| |
These Coq people have version "numbers" that look nothing like numbers, such as "trunk". Also, they didn't test their pull request #188. Fixing this.
|
|\ |
|