aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Update Coq documentationv2.3xleroy2014-05-052-4/+4
* Update for release 2.3.xleroy2014-05-052-2/+3
* Fused multiply-add for IA32.xleroy2014-05-054-4/+45
* Stern warning on non-prototype function definitions.xleroy2014-05-051-0/+1
* Do not allow typedef_name in identifier lists of K&R style definitionsjjourdan2014-05-051-4/+4
* Support for old-style K&R function definitions.xleroy2014-05-056-4545/+5621
* Treat all identifiers as VAR_NAME by default (i.e. if not bound by a typedef)...xleroy2014-05-052-15/+8
* Adapt to the two different calling conventions for floats.xleroy2014-05-026-0/+14
* ARM: honor common variables.xleroy2014-05-022-12/+27
* New sub-target: arm-hardfloatxleroy2014-05-021-0/+11
* Preliminary support for EABI-hardfloat calling conventionsxleroy2014-05-023-48/+938
* Be less picky in the way we parse '#' linesxleroy2014-05-021-11/+23
* Check availability of toolsxleroy2014-05-021-0/+50
* Bump version number before I forgetxleroy2014-05-011-1/+1
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-2949-3224/+66259
* Update with post-2.2 changesxleroy2014-04-231-0/+36
* Clean-up pass on C types:xleroy2014-04-239-135/+381
* Continued: change typeconv t into incrdecr_type t for Epostincr.xleroy2014-04-162-3/+3
* Use "incrdecr_type ty" instead of "typeconv ty" as the intermediate typexleroy2014-04-153-7/+18
* Updated the proofs.xleroy2014-04-121-1/+3
* ia32/Select*: complete the modifications to shifts.xleroy2014-04-115-21/+30
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove...xleroy2014-04-0919-186/+489
* Support Onot operator / notl instruction. More constant propagation during s...xleroy2014-04-0611-26/+100
* Reducing compilation times: (by 35% on one example)xleroy2014-04-061-20/+18
* Merge of branch linear-typing:xleroy2014-04-0619-783/+1787
* "->" can also be applied to array types, not just pointer types.xleroy2014-03-301-1/+1
* __builtin_absfloat can be applied to integers too.xleroy2014-03-293-22/+60
* Inlining: preserve all RTL regs mentioned in the function, not justxleroy2014-03-293-107/+164
* C: Support array initializers that are too short + default init for remainder.xleroy2014-03-2815-197/+605
* Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):xleroy2014-03-289-1522/+672
* Commentsxleroy2014-03-271-0/+7
* Move wt_instr_inv where it belongs.xleroy2014-03-274-21/+21
* Revised division of labor between RTLtyping and Lineartyping:xleroy2014-03-277-661/+1504
* Type-checking of builtin volatile write Mfloat32 was too strict, causing type...xleroy2014-03-242-4/+4
* Error messages were not displayed correctly if the main() function is missing...xleroy2014-03-211-5/+5
* Support array initialization lists that are too shortxleroy2014-03-182-6/+14
* Use .comm to declare uninitialized BSS variables. xleroy2014-03-141-12/+24
* floatoflong_from_words, floatoflongu_from_words : proof of PowerPc implementa...jjourdan2014-03-131-89/+316
* floatoflong_decomp, floatoflongu_decompjjourdan2014-03-111-0/+238
* Force dependency of SelectOp on Compopts.xleroy2014-03-033-1/+3
* Do not transform __builtin_va_arg for a struct or union type, this causesxleroy2014-02-241-31/+37
* Silence the warning "Cannot build inversion information".xleroy2014-02-241-9/+10
* Update clightgen for CompCert 2.2.v2.2xleroy2014-02-233-17/+33
* In Regalloc, dead code elimination, don't eliminate move operationsxleroy2014-02-237-4/+21
* Updates for release 2.2xleroy2014-02-215-11/+34
* Beautify the output.xleroy2014-02-211-3/+7
* Wrong type used for transforming lval = f(...)xleroy2014-02-211-1/+1
* PowerPC is big-endian, dammit.xleroy2014-02-211-2/+2
* Remove useless checks on type_of_global in dynamic semanticsxleroy2014-02-208-74/+15
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-1931-97/+215