aboutsummaryrefslogtreecommitdiffstats
path: root/Changelog
Commit message (Expand)AuthorAgeFilesLines
* MAJ release 2.1v2.1xleroy2013-10-281-10/+25
* Merge of the "alignas" branch.xleroy2013-10-051-0/+5
* Small improvements in compilation times for the register allocation pass.xleroy2013-09-201-0/+2
* Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms xleroy2013-09-141-0/+5
* Change interface of Kildall solvers to avoid precomputing the map pc -> list ...xleroy2013-08-121-1/+1
* Merge of Flocq version 2.2.0.xleroy2013-08-021-0/+2
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-0/+2
* Treat casts int64 -> float32 as primitive operations instead of twoxleroy2013-07-031-0/+8
* Version 2.00 -> version 2.0v2.0xleroy2013-06-211-2/+2
* Updates in preparation for release 2.00xleroy2013-06-191-5/+4
* Updated for release 2.00xleroy2013-06-161-3/+60
* Watch out for behaviors exponential in the nesting of struct/union types. xleroy2013-03-231-0/+2
* More aggressive CSE across Ibuiltin.xleroy2013-03-171-0/+2
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-161-0/+8
* More updates for 1.13xleroy2013-03-111-2/+5
* Updated for version 1.13xleroy2013-03-111-10/+22
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-0/+3
* Finished backtracking (cf previous commit) for ARM and PowerPC.xleroy2013-03-041-1/+2
* Partial backtracking on previous commit: the "hole in Mach stack frame" xleroy2013-03-031-1/+0
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-0/+3
* Constant propagation within __builtin_annot.xleroy2013-02-241-0/+4
* Pointers one pastxleroy2013-02-151-1/+3
* lib/Integers.v: revised and extended, faster implementation based onxleroy2013-02-101-0/+11
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-0/+6
* Update for release 1.12xleroy2013-01-091-2/+13
* Support for inline assembly (asm statements).xleroy2012-12-181-0/+3
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-0/+6
* Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)xleroy2012-11-031-0/+5
* Generate output files in current directory; can be overriden with -o optionxleroy2012-10-081-0/+6
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-6/+22
* More aggressive elimination of conditional branches during constantxleroy2012-08-011-0/+6
* Support for indirect symbols under MacOS X (final).xleroy2012-07-141-0/+8
* Preparation for release 1.11v1.11xleroy2012-07-131-1/+1
* Added option -falign-functionsxleroy2012-07-011-1/+3
* Changelog: updatedxleroy2012-06-281-0/+38
* Make min_int / -1 and min_int % -1 semantically undefinedxleroy2012-06-091-0/+9
* MAJ docv1.10xleroy2012-03-121-1/+1
* Merge of Andrew Tolmach's HASP-related changesxleroy2012-03-091-0/+1
* PowerPC: remove the fmadd and fmsub operators/Asm instructionsxleroy2012-03-071-0/+3
* Added command-line options -Wp,<opt> -Wa,<opt> -Wl,<opt>xleroy2012-02-291-1/+4
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-1/+3
* Translate CompCert C's "a ? b : c" to the equivalent simple Clight expr ifxleroy2012-02-251-2/+2
* More aggressive common subexpression elimination (CSE) of memory loads.xleroy2012-02-231-0/+1
* Simplified and cleaned up the passing of information from C2C to PrintAsm, as...xleroy2012-02-221-0/+35
* Updatev1.9.1xleroy2011-11-271-7/+26
* Changelog, doc: updated for release 1.9v1.9xleroy2011-08-221-1/+1
* Presimplification SimplVolatile: cleaned up and integrated.xleroy2011-08-181-0/+8
* MAJxleroy2011-08-161-4/+12
* ARM: added reversed load/store builtins + bswap builtin (to be tested)xleroy2011-07-301-4/+23
* In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to the...xleroy2011-07-161-0/+5