| Commit message (Expand) | Author | Age |
* | Removed Oandimm, etc, cases, because of 2-address constraints... | xleroy | 2012-05-29 |
* | CSE: add recognition of some combined operators, conditions, and addressing m... | xleroy | 2012-05-26 |
* | Merge of the newmem branch: | xleroy | 2012-05-21 |
* | checklink: first import of Valentin Robert's validator for asm and link | xleroy | 2012-03-28 |
* | Make CPragmas common to all ports. | xleroy | 2012-02-27 |
* | Take advantage of Cmaskzero and Cmasknotzero. | xleroy | 2012-02-24 |
* | More aggressive common subexpression elimination (CSE) of memory loads. | xleroy | 2012-02-23 |
* | Simplified and cleaned up the passing of information from C2C to PrintAsm, as... | xleroy | 2012-02-22 |
* | Merge of the "volatile" branch: | xleroy | 2012-02-04 |
* | Added volatile_read_global and volatile_store_global builtins. | xleroy | 2012-01-15 |
* | Merge of the nonstrict-ops branch: | xleroy | 2012-01-14 |
* | Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml chars | xleroy | 2011-10-18 |
* | Revised emulation of packed structs | xleroy | 2011-10-16 |
* | Watch out for min_int / -1 | xleroy | 2011-08-27 |
* | Cleaned up old commented-out parts | xleroy | 2011-08-19 |
* | More careful treatment of 'load immediate 0' as 'xor self' | xleroy | 2011-08-18 |
* | Forgot to update: adding xchg instruction | xleroy | 2011-08-16 |
* | Locations.v: add Loc.diff_dec. | xleroy | 2011-08-14 |
* | IA32 PrintAsm.ml: wrong moves generated in print_builtin_memcpy_big | xleroy | 2011-08-10 |
* | IA32 port: more faithful treatment of pseudoregister ST0. | xleroy | 2011-08-08 |
* | Cleaned up handling of composite conditions | xleroy | 2011-08-05 |
* | ARM: added reversed load/store builtins + bswap builtin (to be tested) | xleroy | 2011-07-30 |
* | Added animation of the CompCert C semantics (ccomp -interp) | xleroy | 2011-07-28 |
* | Merge of branch new-semantics: revised and strengthened top-level statements ... | xleroy | 2011-07-15 |
* | Revised handling of annotation statements, and more generally built-in functi... | xleroy | 2011-06-13 |
* | Nicer printing of annotations. | xleroy | 2011-05-23 |
* | cparser/StructAssign: always use __builtin_memcpy + alignment indication | xleroy | 2011-05-11 |
* | Added pass CleanupLabels to remove unreferenced labels in a proved way. | xleroy | 2011-05-08 |
* | cparser/Elab: __attribute, not attribute | xleroy | 2011-04-16 |
* | Preliminary support for 'aligned' and 'section' attributes, gcc-style. New-s... | xleroy | 2011-04-16 |
* | Renamed Machconcr into Machsem. | xleroy | 2011-04-09 |
* | Merge of branch "unsigned-offsets": | xleroy | 2011-04-09 |
* | Use movapd instead of movsd for xmm reg-reg move: it avoids partial register ... | xleroy | 2010-11-28 |
* | float->int conversions, continued: weaker axiomatization. | xleroy | 2010-10-29 |
* | Float.intoffloat and Float.intuoffloat are now partial functions. | xleroy | 2010-10-28 |
* | Comments | xleroy | 2010-09-10 |
* | Improvements for int8 and int16 stores | xleroy | 2010-09-10 |
* | Updates for IA32-Cygwin. | xleroy | 2010-09-08 |
* | Update: adding __builtin_annotation | xleroy | 2010-09-04 |
* | Support for __builtin_fmax and __builtin_fmin | xleroy | 2010-09-04 |
* | Merge of the reuse-temps branch: | xleroy | 2010-09-02 |