Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Update the vendored Flocq library to version 3.4.2 | Xavier Leroy | 2021-09-25 | 1 | -0/+4 |
| | | | | For compatibility with the upcoming Coq 8.14. | ||||
* | Update Changelog for release 3.9 | Xavier Leroy | 2021-05-09 | 1 | -0/+3 |
| | |||||
* | Update Changelog | Xavier Leroy | 2021-05-08 | 1 | -1/+11 |
| | |||||
* | Update Changelog | Xavier Leroy | 2021-04-29 | 1 | -0/+53 |
| | |||||
* | Updates for release 3.8v3.8 | Xavier Leroy | 2020-11-16 | 1 | -0/+3 |
| | |||||
* | Support Coq 8.12.1 | Xavier Leroy | 2020-11-14 | 1 | -1/+1 |
| | |||||
* | Update Changes | Xavier Leroy | 2020-11-08 | 1 | -0/+48 |
| | |||||
* | Updates for release 3.7 | Xavier Leroy | 2020-03-31 | 1 | -0/+3 |
| | |||||
* | Update Changelog | Xavier Leroy | 2020-03-31 | 1 | -3/+34 |
| | |||||
* | Support Coq 8.11.0 (#212) | Xavier Leroy | 2020-02-05 | 1 | -0/+4 |
| | | | | Update configure. Ignore and clean up .vok and .vos files, which Coq 8.11.0 generates. | ||||
* | Updates in preparation for release 3.6 | Xavier Leroy | 2019-09-16 | 1 | -0/+62 |
| | |||||
* | Update Changelog in preparation for release 3.5 | Xavier Leroy | 2019-02-26 | 1 | -1/+1 |
| | |||||
* | Update Changelog in preparation for release 3.5 | Xavier Leroy | 2019-02-25 | 1 | -0/+35 |
| | |||||
* | Updates for release 3.4v3.4 | Xavier Leroy | 2018-09-17 | 1 | -1/+1 |
| | |||||
* | Update change log for 3.4, continued | Xavier Leroy | 2018-09-14 | 1 | -2/+5 |
| | |||||
* | Typo in OCaml version number | Xavier Leroy | 2018-09-12 | 1 | -1/+1 |
| | |||||
* | Update version and change log in preparation for public release 3.4 | Xavier Leroy | 2018-09-12 | 1 | -0/+62 |
| | |||||
* | Changelog: minor updates for 3.3 | Xavier Leroy | 2018-05-30 | 1 | -7/+4 |
| | |||||
* | Mention optional installation of .vo files | Xavier Leroy | 2018-05-30 | 1 | -0/+3 |
| | |||||
* | Updates for public release 3.3 | Xavier Leroy | 2018-05-30 | 1 | -0/+72 |
| | |||||
* | Preparations for release 3.2 | Xavier Leroy | 2018-01-13 | 1 | -2/+5 |
| | |||||
* | Update Changelog with recent changes | Xavier Leroy | 2018-01-11 | 1 | -1/+13 |
| | |||||
* | Coq 8.7.1 support | Xavier Leroy | 2017-12-18 | 1 | -2/+3 |
| | | | | It is compatible with 8.7.0 and 8.6.1, no changes required to the Coq sources of CompCert. | ||||
* | Issue #208: make value analysis of comparisons more conservative w.r.t. ↵ | Xavier Leroy | 2017-11-24 | 1 | -0/+3 |
| | | | | | | | pointers (#209) Comparisons such as "(uintptr_t) &global == 0x1234" are undefined behavior in CompCert but their status in ISO C is unclear and they may occur in real-world code. Make sure they are statically analyzed as Btop. | ||||
* | Pull request #192: improve the printing of Clight intermediate code | Xavier Leroy | 2017-11-22 | 1 | -0/+2 |
| | | | | So that it looks more like valid C source. | ||||
* | Coq 8.7.0 support | Xavier Leroy | 2017-10-20 | 1 | -0/+5 |
| | | | | | | configure: accept Coq 8.7.0 and 8.6.1. (Coq 8.6 became incompatible with commit b4f59c4.) Changelog: updated. | ||||
* | Resurrect the Cygwin x86-32 port | Xavier Leroy | 2017-09-11 | 1 | -0/+3 |
| | | | | It got lost during the addition of the x86-64 port in release 3.0. | ||||
* | ARM in Thumb mode: simpler instruction sequence for Pbtbl pseudo | Xavier Leroy | 2017-08-22 | 1 | -0/+4 |
| | | | | It is also easier to recognize than the old one for binary analysis tools. | ||||
* | Issue P #25: make sure sizeof(long double) = sizeof(double) in all contexts. | Xavier Leroy | 2017-08-22 | 1 | -0/+3 |
| | |||||
* | Update Changelog in preparation for release 3.1 | Xavier Leroy | 2017-08-18 | 1 | -2/+8 |
| | |||||
* | Issue #196: excessive proof-checking times in .v files generated by clightgen | Xavier Leroy | 2017-08-15 | 1 | -0/+1 |
| | | | | | | The check that "build_composite_env composites = OK (make_composite_env composites)" is taking time exponential on the number of struct/union definitions, at least on the example provided in #196. The solution implemented in this commit is to use computational reflection more efficiently, just to check that "build_composite_env composites" is of the form "OK _". From there, a new function Clightdefs.mkprogram produces the appropriate Clight.program without additional computation. | ||||
* | Update Changelog with news since release 3.0.1 | Xavier Leroy | 2017-07-27 | 1 | -4/+29 |
| | |||||
* | Issue #16P: wrong rlwinm instruction generated by constant propagation | Xavier Leroy | 2017-07-05 | 1 | -2/+4 |
| | | | | This happens when the divisor of an unsigned int32 division is constant-propagated to 1. | ||||
* | Update Changelog for clightgen | Xavier Leroy | 2017-06-12 | 1 | -0/+1 |
| | |||||
* | Update Changelog with recent changes | Xavier Leroy | 2017-04-28 | 1 | -1/+7 |
| | |||||
* | RISC-V port and assorted changes | Xavier Leroy | 2017-04-28 | 1 | -0/+2 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes. The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/ This port required the following additional changes: - Integers: More properties about shrx - SelectOp: now provides smart constructors for mulhs and mulhu - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu. - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library. - test/: add SIMU make variable to run tests through a simulator - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers commit da14495c01cf4f66a928c2feff5c53f09bde837f Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Thu Apr 13 17:36:10 2017 +0200 RISC-V port, continued Now working on Asmgen. commit 36f36eb3a5abfbb8805960443d087b6a83e86005 Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Wed Apr 12 17:26:39 2017 +0200 RISC-V port, first steps This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress. | ||||
* | Issue #179: clightgen produces wrong abstract syntax for "switch" statements | Xavier Leroy | 2017-04-28 | 1 | -0/+3 |
| | |||||
* | Remove tests involving Cminor concrete syntax. Update Changelog | Xavier Leroy | 2017-02-15 | 1 | -0/+3 |
| | | | | Follow-up to [29653ba] | ||||
* | Release 3.0.1 here we comev3.0.1 | Xavier Leroy | 2017-02-14 | 1 | -0/+6 |
| | |||||
* | Release 3.0 here we comev3.0 | Xavier Leroy | 2017-02-10 | 1 | -1/+2 |
| | |||||
* | Changelog update concerning attribute handling | Xavier Leroy | 2017-02-07 | 1 | -0/+7 |
| | |||||
* | Update Changes for release 3.0 | Xavier Leroy | 2017-01-31 | 1 | -2/+39 |
| | |||||
* | Documentation updates to mention 64-bit mode and x86_64 port | Xavier Leroy | 2016-10-27 | 1 | -2/+24 |
| | |||||
* | Update Changelog for release 2.7.1v2.7.1 | Xavier Leroy | 2016-07-18 | 1 | -2/+8 |
| | |||||
* | Port to Coq 8.5pl2 | Xavier Leroy | 2016-07-08 | 1 | -0/+6 |
| | | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality. | ||||
* | Changelog update: mention -g for ARM and IA32 | Xavier Leroy | 2016-06-30 | 1 | -0/+4 |
| | |||||
* | Update in preparation for release 2.7 | Xavier Leroy | 2016-06-22 | 1 | -0/+46 |
| | |||||
* | The return type of __builtin_clz() et al is "int", as documented and for GCC ↵v2.6 | Xavier Leroy | 2015-12-21 | 1 | -0/+2 |
| | | | | compatibility, and not "unsigned int", as previously implemented. | ||||
* | Update Changelog for release 2.6. | Xavier Leroy | 2015-12-19 | 1 | -0/+49 |
| | |||||
* | More updates for release 2.5. | Xavier Leroy | 2015-06-11 | 1 | -4/+5 |
| |