summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Merge of Andrew Tolmach's HASP-related changesGravatar xleroy2012-03-09
* Cprint: export Cprint.attributesGravatar xleroy2012-03-07
* PowerPC: remove the fmadd and fmsub operators/Asm instructionsGravatar xleroy2012-03-07
* Add -toolprefixGravatar xleroy2012-03-06
* UpdateGravatar xleroy2012-03-06
* Remove 'near-code' access mode, makes no sense in CompCertGravatar xleroy2012-03-06
* Added command-line options -Wp,<opt> -Wa,<opt> -Wl,<opt>Gravatar xleroy2012-02-29
* Problems with multiple declarations of publically-visible identifiersGravatar xleroy2012-02-29
* Better printing of pointer values and of locations.Gravatar xleroy2012-02-29
* 'typeof' is not a keywordGravatar xleroy2012-02-29
* Make CPragmas common to all ports.Gravatar xleroy2012-02-27
* - Support for _Alignof(ty) operator from ISO C 2011Gravatar xleroy2012-02-26
* Translate CompCert C's "a ? b : c" to the equivalent simple Clight expr ifGravatar xleroy2012-02-25
* Take advantage of Cmaskzero and Cmasknotzero.Gravatar xleroy2012-02-24
* Improved instruction selection for "notint".Gravatar xleroy2012-02-24
* More aggressive common subexpression elimination (CSE) of memory loads.Gravatar xleroy2012-02-23
* Simplified and cleaned up the passing of information from C2C to PrintAsm, as...Gravatar xleroy2012-02-22
* The C declaration associated with __stringlit_N globals now has type const ch...Gravatar xleroy2012-02-20
* Don't print external declarations for builtins.Gravatar xleroy2012-02-18
* Work around limited excursion of conditional branchesGravatar xleroy2012-02-13
* Interp: help debug stuck expressionsGravatar xleroy2012-02-10
* Initializers: handle By_copy accesses (e.g. for &(glob.field))Gravatar xleroy2012-02-07
* Merge of the "volatile" branch:Gravatar xleroy2012-02-04
* Out-of-bounds error in testGravatar xleroy2012-01-21
* Another typo in print_builtin_vstore_commonGravatar xleroy2012-01-21
* Typo in print_builtin_vstore_commonGravatar xleroy2012-01-21
* powerpc/SelectOp: optimize the pattern ((x >>s N) & N1) & N2 common in a cert...Gravatar xleroy2012-01-21
* Cosmetic cleanups.Gravatar xleroy2012-01-15
* Added volatile_read_global and volatile_store_global builtins.Gravatar xleroy2012-01-15
* Merge of the nonstrict-ops branch:Gravatar xleroy2012-01-14
* UpdateGravatar xleroy2011-11-27
* More careful updating of current location for error msgs.Gravatar xleroy2011-11-26
* cparser/*: refactoring of the expansion of read-modify-write operatorsGravatar xleroy2011-11-26
* Fixed serious bug in handling of volatile arrays.Gravatar xleroy2011-11-26
* Interp: accommodate "int main(int, char **)".Gravatar xleroy2011-10-19
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsGravatar xleroy2011-10-18
* Corrected initialization of char arrays by string literals.Gravatar xleroy2011-10-17
* More cleanups in packed struct emulation.Gravatar xleroy2011-10-16
* Revised emulation of packed structsGravatar xleroy2011-10-16
* Watch out for min_int / -1Gravatar xleroy2011-08-27
* Doc fixesGravatar xleroy2011-08-23
* MAJ licenceGravatar xleroy2011-08-23
* Changelog, doc: updated for release 1.9Gravatar xleroy2011-08-22
* arm/PrintAsm: don't generate "vfd" directive, useless?Gravatar xleroy2011-08-22
* Harden proof script against empty destroyed_at_moveGravatar xleroy2011-08-22
* Wrong check: &e must be rejected if e has array type and is not a l-value.Gravatar xleroy2011-08-21
* Cleaned up old commented-out partsGravatar xleroy2011-08-19
* More careful treatment of 'load immediate 0' as 'xor self'Gravatar xleroy2011-08-18
* Presimplification SimplVolatile: cleaned up and integrated.Gravatar xleroy2011-08-18
* SimplVolatile: new pass to eliminate read-modify-write ops over volatilesGravatar xleroy2011-08-18