| Commit message (Expand) | Author | Age |
* | Refactoring: move definition of chunk_of_type to AST.v. | xleroy | 2013-05-06 |
* | Syntax errors | xleroy | 2013-05-06 |
* | Wrong pseudo-instr | xleroy | 2013-05-06 |
* | Support for in64 -> float conversions w/ correct rounding. | xleroy | 2013-05-06 |
* | ia32/i64_dtou: wrong play on rounding mode | xleroy | 2013-05-05 |
* | Extend CSE of loads following stores to chunks Mint64 and Mfloat64al32. | xleroy | 2013-05-02 |
* | Stack-align to 8 arguments of Tfloat and Tlong types, as per the SVR4 ABI and... | xleroy | 2013-05-02 |
* | Clean up 'make clean' | xleroy | 2013-05-01 |
* | Use "-as" to put CompCert modules in a compcert.xxx namespace. | xleroy | 2013-05-01 |
* | Oops, removed a crucial declaration for Allocation. | xleroy | 2013-05-01 |
* | Coq-defined equality functions for Allocation. (continued) | xleroy | 2013-05-01 |
* | Coq-defined equality functions for Allocation. | xleroy | 2013-05-01 |
* | Removing modules now unused | xleroy | 2013-05-01 |
* | Add bswap16 | xleroy | 2013-04-30 |
* | Updated to Pbuiltin with list of results | xleroy | 2013-04-30 |
* | Updated to new CminorSel | xleroy | 2013-04-30 |
* | Typos in comments | xleroy | 2013-04-30 |
* | Updated | xleroy | 2013-04-30 |
* | Expand 64-bit integer comparisons into 32-bit integer comparisons. | xleroy | 2013-04-29 |
* | Decomposing 64-bit "less than" comparisons. | xleroy | 2013-04-29 |
* | Revert suppression of __builtin_{read,write}_reversed for x86 and ARM, | xleroy | 2013-04-29 |
* | Missing GLOB | xleroy | 2013-04-23 |
* | Make ia32/ code more portable across systems. | xleroy | 2013-04-23 |
* | driver: removed option -flonglong | xleroy | 2013-04-22 |
* | Results for ARM | xleroy | 2013-04-22 |
* | Labeled statements inside switch were incorrectly processed. | xleroy | 2013-04-22 |
* | Deactivate combination Aindexed 0 / Oadd, as it causes problems with chunk = ... | xleroy | 2013-04-21 |
* | Fixes in PowerPC port | xleroy | 2013-04-21 |
* | Add __builtin_bswap16 and __builtin_bswap32 to all ports. | xleroy | 2013-04-20 |
* | Rename arm/linux into arm/eabi, more descriptive. | xleroy | 2013-04-20 |
* | Split arch/int64.s into one file per function. | xleroy | 2013-04-20 |
* | Configuring the assembler used for the runtime lib | xleroy | 2013-04-20 |
* | Remove __i64_{neg,add,sub,mul}, now handled directly by the compiler. | xleroy | 2013-04-20 |
* | Added FFTW benchmark provided by Guillaume Melquiond | xleroy | 2013-04-20 |
* | Tests "floats" and "floats-basics" moved from test/c to test/regression | xleroy | 2013-04-20 |
* | Interp.ml: support printf of long long | xleroy | 2013-04-20 |
* | Big merge of the newregalloc-int64 branch. Lots of changes in two directions: | xleroy | 2013-04-20 |
* | Updated issues with coqchk. See PR#3026 on the Coq bug tracker. | xleroy | 2013-04-14 |
* | List.iteri not in OCaml < 4.00, better not use it. | xleroy | 2013-04-08 |
* | Updated | xleroy | 2013-03-26 |
* | Error when calling un-prototyped function. | xleroy | 2013-03-25 |
* | Better locations for error messages relative to type specifiers. | xleroy | 2013-03-25 |
* | Watch out for behaviors exponential in the nesting of struct/union types. | xleroy | 2013-03-23 |
* | RTLtyping: now performed entirely in Coq, no need for an external Caml oracle... | xleroy | 2013-03-22 |
* | Update clightgen to changes in Camlcoq and in AST. | xleroy | 2013-03-20 |
* | Diab asm syntax issue | xleroy | 2013-03-20 |
* | For Pfreeframe, generate an "addi" over GPR1 when possible, to work around a ... | xleroy | 2013-03-18 |
* | Remove the C primitives for unsigned long long arithmetic, replaced | xleroy | 2013-03-18 |
* | More aggressive CSE across Ibuiltin. | xleroy | 2013-03-17 |
* | Assorted changes to reduce stack and heap requirements when compiling very bi... | xleroy | 2013-03-16 |