aboutsummaryrefslogtreecommitdiffstats
path: root/Changelog
Commit message (Collapse)AuthorAgeFilesLines
* Second update for release 3.10Xavier Leroy2021-11-191-4/+6
|
* First update for release 3.10Xavier Leroy2021-11-161-0/+55
|
* Update the vendored Flocq library to version 3.4.2Xavier Leroy2021-09-251-0/+4
| | | | For compatibility with the upcoming Coq 8.14.
* Update Changelog for release 3.9Xavier Leroy2021-05-091-0/+3
|
* Update ChangelogXavier Leroy2021-05-081-1/+11
|
* Update ChangelogXavier Leroy2021-04-291-0/+53
|
* Updates for release 3.8v3.8Xavier Leroy2020-11-161-0/+3
|
* Support Coq 8.12.1Xavier Leroy2020-11-141-1/+1
|
* Update ChangesXavier Leroy2020-11-081-0/+48
|
* Updates for release 3.7Xavier Leroy2020-03-311-0/+3
|
* Update ChangelogXavier Leroy2020-03-311-3/+34
|
* Support Coq 8.11.0 (#212)Xavier Leroy2020-02-051-0/+4
| | | | Update configure. Ignore and clean up .vok and .vos files, which Coq 8.11.0 generates.
* Updates in preparation for release 3.6Xavier Leroy2019-09-161-0/+62
|
* Update Changelog in preparation for release 3.5Xavier Leroy2019-02-261-1/+1
|
* Update Changelog in preparation for release 3.5Xavier Leroy2019-02-251-0/+35
|
* Updates for release 3.4v3.4Xavier Leroy2018-09-171-1/+1
|
* Update change log for 3.4, continuedXavier Leroy2018-09-141-2/+5
|
* Typo in OCaml version numberXavier Leroy2018-09-121-1/+1
|
* Update version and change log in preparation for public release 3.4Xavier Leroy2018-09-121-0/+62
|
* Changelog: minor updates for 3.3Xavier Leroy2018-05-301-7/+4
|
* Mention optional installation of .vo filesXavier Leroy2018-05-301-0/+3
|
* Updates for public release 3.3Xavier Leroy2018-05-301-0/+72
|
* Preparations for release 3.2Xavier Leroy2018-01-131-2/+5
|
* Update Changelog with recent changesXavier Leroy2018-01-111-1/+13
|
* Coq 8.7.1 supportXavier Leroy2017-12-181-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 Leroy2017-11-241-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 codeXavier Leroy2017-11-221-0/+2
| | | | So that it looks more like valid C source.
* Coq 8.7.0 supportXavier Leroy2017-10-201-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 portXavier Leroy2017-09-111-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 pseudoXavier Leroy2017-08-221-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 Leroy2017-08-221-0/+3
|
* Update Changelog in preparation for release 3.1Xavier Leroy2017-08-181-2/+8
|
* Issue #196: excessive proof-checking times in .v files generated by clightgenXavier Leroy2017-08-151-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.1Xavier Leroy2017-07-271-4/+29
|
* Issue #16P: wrong rlwinm instruction generated by constant propagationXavier Leroy2017-07-051-2/+4
| | | | This happens when the divisor of an unsigned int32 division is constant-propagated to 1.
* Update Changelog for clightgenXavier Leroy2017-06-121-0/+1
|
* Update Changelog with recent changesXavier Leroy2017-04-281-1/+7
|
* RISC-V port and assorted changesXavier Leroy2017-04-281-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" statementsXavier Leroy2017-04-281-0/+3
|
* Remove tests involving Cminor concrete syntax. Update ChangelogXavier Leroy2017-02-151-0/+3
| | | | Follow-up to [29653ba]
* Release 3.0.1 here we comev3.0.1Xavier Leroy2017-02-141-0/+6
|
* Release 3.0 here we comev3.0Xavier Leroy2017-02-101-1/+2
|
* Changelog update concerning attribute handlingXavier Leroy2017-02-071-0/+7
|
* Update Changes for release 3.0Xavier Leroy2017-01-311-2/+39
|
* Documentation updates to mention 64-bit mode and x86_64 portXavier Leroy2016-10-271-2/+24
|
* Update Changelog for release 2.7.1v2.7.1Xavier Leroy2016-07-181-2/+8
|
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-0/+6
| | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* Changelog update: mention -g for ARM and IA32Xavier Leroy2016-06-301-0/+4
|
* Update in preparation for release 2.7Xavier Leroy2016-06-221-0/+46
|
* The return type of __builtin_clz() et al is "int", as documented and for GCC ↵v2.6Xavier Leroy2015-12-211-0/+2
| | | | compatibility, and not "unsigned int", as previously implemented.
generated by cgit (git 2.34.1) at 2024-05-08 11:50:13 +0000