aboutsummaryrefslogtreecommitdiffstats
path: root/Changelog
Commit message (Expand)AuthorAgeFilesLines
...
* 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
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-0/+8
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-0/+12
* Forgot somethingxleroy2011-05-241-0/+4
* Update for release 1.8.2xleroy2011-05-241-0/+3
* cparser: support for attributes over struct and union.xleroy2011-05-121-2/+4
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).xleroy2011-05-081-0/+26
* Update for 1.8.1 releasev1.8.1xleroy2011-03-141-0/+23
* Update for release 1.8xleroy2010-09-211-6/+7
* Updatedxleroy2010-09-041-9/+25
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-0/+7
* Updatexleroy2010-05-051-1/+24
* Update for 1.7.1v1.7.1xleroy2010-04-131-0/+17
* Updates for release 1.7v1.7xleroy2010-03-301-0/+46
* Backtracking on commit 1220v1.6xleroy2010-01-131-1/+1