Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Towards supporting the CompCert tests (not finished) | Cyril SIX | 2019-06-14 | 1 | -0/+2 |
| | |||||
* | Merge branch 'mppa-work' into mppa-abstractbb-dev | Sylvain Boulmé | 2019-06-08 | 1 | -11/+30 |
|\ | |||||
| * | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵ | David Monniaux | 2019-06-03 | 1 | -5/+11 |
| |\ | | | | | | | | | | mppa-if-conversion | ||||
| | * | Coq 8.9.1 support | Xavier Leroy | 2019-05-21 | 1 | -3/+3 |
| | | | | | | | | | | | | It works fine with the current sources. | ||||
| | * | Upgrade embedded version of Flocq to 3.1. | Guillaume Melquiond | 2019-03-27 | 1 | -2/+2 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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). | ||||
| | * | Harden configure against weird Menhir installations | Xavier Leroy | 2019-03-25 | 1 | -2/+8 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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`. | ||||
| * | | fix variable issue | David Monniaux | 2019-05-29 | 1 | -1/+1 |
| | | | |||||
| * | | adaptation pour k1c-cos | David Monniaux | 2019-05-28 | 1 | -6/+19 |
| | | | |||||
* | | | extending bblock_simu_test with rewriting | Sylvain Boulmé | 2019-05-26 | 1 | -1/+1 |
|/ / | |||||
* | | oubli DecBoolOps.v | David Monniaux | 2019-05-06 | 1 | -1/+1 |
| | | |||||
* | | Fixing Coq dependencies | Cyril SIX | 2019-05-03 | 1 | -1/+1 |
| | | |||||
* | | cleaner: put all the special types, defines etc. in one header file | David Monniaux | 2019-04-11 | 1 | -1/+1 |
| | | |||||
* | | Integrating Asmvliw.v in the proof chain | Cyril SIX | 2019-03-20 | 1 | -1/+1 |
| | | |||||
* | | Merge branch 'master' into mppa_postpass | Cyril SIX | 2019-03-13 | 1 | -5/+6 |
|\| | | | | | | | | | | | Conflicts: .gitignore runtime/include/stdbool.h | ||||
| * | Maximum supported Menhir version (#275) | Xavier Leroy | 2019-02-26 | 1 | -1/+1 |
| | | | | | | | | | | Follow-up to commit fc9bc643. The latest Menhir version compatible with the current code base is actually 20181113. | ||||
| * | Maximum supported Menhir version (#275) | Jacques-Henri Jourdan | 2019-02-25 | 1 | -2/+3 |
| | | | | | | 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). | ||||
| * | Add support for Coq 8.9.0 | Xavier Leroy | 2019-02-04 | 1 | -3/+3 |
| | | | | | | | | No other changes are needed to support 8.9.0. | ||||
* | | Plugged Asmblockdeps into PostpassScheduling | Cyril SIX | 2019-02-25 | 1 | -0/+1 |
| | | |||||
* | | Added AbstractBasicBlock files to the Coq build process | Cyril SIX | 2019-02-13 | 1 | -4/+6 |
| | | |||||
* | | pour ne plus être embêtés avec le int128 | David Monniaux | 2019-01-30 | 1 | -1/+1 |
| | | |||||
* | | no __SIZEOF_INT128__ | David Monniaux | 2019-01-30 | 1 | -1/+1 |
| | | | | | | | | J'avais fait une erreur, les __SSE__ c'était quand je compilais sur x86. | ||||
* | | Rajouté -U__SSE__ -U__SSE2__ dans le ./configure pour le K1 | Cyril SIX | 2019-01-30 | 1 | -1/+1 |
| | | |||||
* | | configure: improve preprocessor options | Sylvain Boulmé | 2019-01-18 | 1 | -1/+1 |
| | | |||||
* | | fix oubli dans configure | Sylvain Boulmé | 2019-01-18 | 1 | -1/+1 |
| | | |||||
* | | BROKEN - works for x86, not for k1 anymore | Cyril SIX | 2018-11-26 | 1 | -0/+3 |
| | | |||||
* | | Moved some files to mppa_k1c/lib ; reworked configure and Makefile to allow that | Cyril SIX | 2018-11-26 | 1 | -0/+6 |
| | | |||||
* | | Merge tag 'v3.4' into mppa_k1c | Cyril SIX | 2018-11-21 | 1 | -8/+51 |
|\| | | | | | | | | | Conflicts: .gitignore | ||||
| * | Tentatively support Coq 8.8.2 | Xavier Leroy | 2018-09-12 | 1 | -2/+2 |
| | | | | | | | | | | 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. | ||||
| * | Improve reporting of configuration errors | Xavier Leroy | 2018-08-28 | 1 | -0/+10 |
| | | | | | | | | | | | | | | | | | | | | | | | | 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 `-`). | ||||
| * | Remove leftover Makefile.config before configuration | Xavier Leroy | 2018-08-28 | 1 | -0/+4 |
| | | | | | | | | | | | | | | So that if an error occurs during configuration, there is no Makefile.config file and "make" will fail. Closes: #244 | ||||
| * | Support Coq 8.8.1 (#242) | Xavier Leroy | 2018-07-10 | 1 | -3/+3 |
| | | |||||
| * | Ensure compatibility with Menhir before and after version 20180530 | Xavier Leroy | 2018-06-06 | 1 | -3/+9 |
| | | | | | | | | Inspired by and adapted from pull request #235 by Benoît Viguier. | ||||
| * | Fix menhirLib namespaces, following changes in Menhir version 20180530 | Jacques-Henri Jourdan | 2018-06-06 | 1 | -1/+1 |
| | | |||||
| * | Install Coq development (.vo files) if requested (#232) | Xavier Leroy | 2018-05-30 | 1 | -3/+26 |
| | | | | | | | | | | | | | | | | | | .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 | ||||
| * | Support Coq version 8.8.0 | Xavier Leroy | 2018-04-25 | 1 | -3/+3 |
| | | |||||
* | | Fixing k1-gcc becoming k1-mbr-gcc | Cyril SIX | 2018-11-09 | 1 | -5/+6 |
| | | |||||
* | | Fixed CompCert library inclusion. Indirect fix for udivd and umodd | Cyril SIX | 2018-06-26 | 1 | -1/+3 |
| | | |||||
* | | MPPA - Fixed -m64 missing | Cyril SIX | 2018-04-26 | 1 | -1/+1 |
| | | |||||
* | | Hook for MPPA_K1c (generates Risc-V code for now) | Cyril SIX | 2018-04-04 | 1 | -0/+22 |
|/ | |||||
* | Support Coq 8.7.2 | Xavier Leroy | 2018-02-19 | 1 | -3/+3 |
| | |||||
* | Removed struct passing/return from Configurations | Bernhard Schommer | 2018-02-16 | 1 | -40/+0 |
| | |||||
* | Rename abi for ppc-linux targets. | Bernhard Schommer | 2018-02-16 | 1 | -2/+2 |
| | |||||
* | Fix typo in comment | Michael Schmidt | 2018-02-16 | 1 | -1/+1 |
| | |||||
* | Add support for x86_64 BSD (#56) | Xavier Leroy | 2018-02-09 | 1 | -3/+19 |
| | |||||
* | Configure check for PIE (#55) | Michael Schmidt | 2018-02-08 | 1 | -5/+12 |
| | | | | | When checking for -no-pie and -nopie, evaluate gcc output for error message like 'unknown argument'. (Relying on the error code is not enough.) | ||||
* | Removed superfluous check. | Bernhard Schommer | 2018-02-06 | 1 | -4/+0 |
| | |||||
* | Improved message recommending an OCaml version to use | Xavier Leroy | 2018-01-13 | 1 | -1/+1 |
| | |||||
* | Resynchronize the LICENSE file and the license headers in individual files (#45) | Xavier Leroy | 2018-01-05 | 1 | -0/+3 |
| | | | | | | | | | | | 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/ | ||||
* | Coq 8.7.1 support | Xavier Leroy | 2017-12-18 | 1 | -3/+3 |
| | | | | It is compatible with 8.7.0 and 8.6.1, no changes required to the Coq sources of CompCert. | ||||
* | Coq 8.7.0 support | Xavier Leroy | 2017-10-20 | 1 | -3/+3 |
| | | | | | | configure: accept Coq 8.7.0 and 8.6.1. (Coq 8.6 became incompatible with commit b4f59c4.) Changelog: updated. |