aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Deactivate combination Aindexed 0 / Oadd, as it causes problems with chunk = ...xleroy2013-04-212-4/+0
* Fixes in PowerPC portxleroy2013-04-2111-322/+392
* Add __builtin_bswap16 and __builtin_bswap32 to all ports.xleroy2013-04-2014-136/+128
* Rename arm/linux into arm/eabi, more descriptive.xleroy2013-04-203-3/+4
* Split arch/int64.s into one file per function.xleroy2013-04-2045-1238/+2698
* Configuring the assembler used for the runtime libxleroy2013-04-203-2/+12
* Remove __i64_{neg,add,sub,mul}, now handled directly by the compiler.xleroy2013-04-204-171/+0
* Added FFTW benchmark provided by Guillaume Melquiondxleroy2013-04-203-2/+107
* Tests "floats" and "floats-basics" moved from test/c to test/regressionxleroy2013-04-207-21/+18
* Interp.ml: support printf of long longxleroy2013-04-206-60/+4197
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-20166-10626/+20598
* Updated issues with coqchk. See PR#3026 on the Coq bug tracker.xleroy2013-04-141-6/+9
* List.iteri not in OCaml < 4.00, better not use it.xleroy2013-04-081-2/+9
* Updatedxleroy2013-03-262-18/+23
* Error when calling un-prototyped function.xleroy2013-03-251-6/+8
* Better locations for error messages relative to type specifiers.xleroy2013-03-251-14/+9
* Watch out for behaviors exponential in the nesting of struct/union types. xleroy2013-03-236-66/+78
* RTLtyping: now performed entirely in Coq, no need for an external Caml oracle...xleroy2013-03-223-374/+713
* Update clightgen to changes in Camlcoq and in AST.xleroy2013-03-202-15/+33
* Diab asm syntax issuexleroy2013-03-201-1/+1
* For Pfreeframe, generate an "addi" over GPR1 when possible, to work around a ...xleroy2013-03-182-3/+13
* Remove the C primitives for unsigned long long arithmetic, replacedxleroy2013-03-184-53/+25
* More aggressive CSE across Ibuiltin.xleroy2013-03-173-7/+36
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-1635-237/+534
* Machsem: no longer useful.xleroy2013-03-141-259/+0
* Bind some local defs with Let, makes extracted code cleanerv1.13xleroy2013-03-121-2/+2
* Maps: revised TREE interface; added mucho derived properties and operations i...xleroy2013-03-122-63/+256
* Suppress int64_unsigned_to_float, now unused.xleroy2013-03-112-7/+0
* More updates for 1.13xleroy2013-03-111-2/+5
* Fixed parsing of hex float literals 0xNNNpMMM.xleroy2013-03-115-4/+81
* Updated for version 1.13xleroy2013-03-112-11/+24
* Updating doc for 1.13xleroy2013-03-111-8/+5
* Useless Importxleroy2013-03-101-1/+0
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-1029-120/+133
* Assorted cleanups, esp. to avoid generating _rec and _rect recursors in xleroy2013-03-0910-215/+260
* Improving the performance of exhaustive exploration (mode -all):xleroy2013-03-091-18/+112
* Finished backtracking (cf previous commit) for ARM and PowerPC.xleroy2013-03-047-815/+593
* Partial backtracking on previous commit: the "hole in Mach stack frame" xleroy2013-03-037-857/+757
* Updates to follow recent changes in PrintAsm.mlxleroy2013-03-011-14/+43
* Some builtins were renamed, updatingxleroy2013-03-011-4/+4
* Bug in Pbtblxleroy2013-03-011-1/+1
* No longer a dependency on Machtypingxleroy2013-03-012-2/+1
* Fix 'interp' entryxleroy2013-03-011-1/+1
* Testing dense switchesxleroy2013-03-013-1/+62
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-0126-7039/+4809
* Updated ARM and PowerPC ports with new handling of __builtin_annot.xleroy2013-02-249-90/+93
* Constant propagation within __builtin_annot.xleroy2013-02-2415-124/+250
* Pointers one pastxleroy2013-02-1521-324/+565
* Updated PowerPC port to new integers.xleroy2013-02-128-29/+59
* Be more like gcc in the way we display or not the usage message.xleroy2013-02-121-8/+6