aboutsummaryrefslogtreecommitdiffstats
path: root/ia32
Commit message (Expand)AuthorAgeFilesLines
* Fused multiply-add for IA32.xleroy2014-05-052-0/+35
* ia32/Select*: complete the modifications to shifts.xleroy2014-04-112-12/+20
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove...xleroy2014-04-094-86/+138
* Support Onot operator / notl instruction. More constant propagation during s...xleroy2014-04-0611-26/+100
* Use .comm to declare uninitialized BSS variables. xleroy2014-03-141-12/+24
* Force dependency of SelectOp on Compopts.xleroy2014-03-031-0/+1
* In Regalloc, dead code elimination, don't eliminate move operationsxleroy2014-02-231-0/+3
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-193-0/+3
* Recognize .i and .p source files as C sources not to be preprocessed.xleroy2014-02-051-0/+1
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-125-17/+9
* Introduce and use the platform-specific Archi module giving:xleroy2014-01-031-5/+13
* Updated neededness analysis for IA32.xleroy2014-01-021-37/+60
* Updated ARM backend wrt new static analyses and optimizations.xleroy2014-01-021-0/+12
* Fine hair splitting depending on whether va_list is a scalar type (IA32, ARM)...xleroy2014-01-011-0/+1
* Experimental support for <stdarg.h>, the GCC way. Works on IA32. To be test...xleroy2014-01-012-2/+27
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-6/+1
* Future-proofing: keep signature information in IA32 and PowerPC Asm, just lik...xleroy2013-12-266-63/+67
* Merge of branch value-analysis.xleroy2013-12-209-504/+720
* Rename "-fno-sse" into "-fno-fpu" and honor it on PowerPC as well.xleroy2013-11-271-1/+1
* Cminor parsing and printing (from Andrew Tolmach)xleroy2013-10-161-0/+1
* Do not use Format for faster printing of RTL, XTL, LTL, Machxleroy2013-09-261-1/+1
* Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms xleroy2013-09-145-25/+84
* Merge of Flocq version 2.2.0.xleroy2013-08-021-0/+28
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-299-16/+78
* More accurate model of condition register flags for ARM and IA32.xleroy2013-07-132-71/+38
* Merge of the "princeton" branch:xleroy2013-06-164-5/+5
* powerpc: tentative support for Diab debug infoxleroy2013-05-201-0/+1
* Merge of the float32 branch: xleroy2013-05-198-40/+51
* Add option -fno-tailcalls to turn off tailcall elimination (causes problem wi...xleroy2013-05-171-2/+1
* Preliminary support for debugging info (-g).xleroy2013-05-171-5/+53
* Refactoring: move definition of chunk_of_type to AST.v.xleroy2013-05-061-3/+0
* Coq-defined equality functions for Allocation.xleroy2013-05-011-5/+11
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-292-7/+6
* Revert suppression of __builtin_{read,write}_reversed for x86 and ARM,xleroy2013-04-293-3/+38
* Add __builtin_bswap16 and __builtin_bswap32 to all ports.xleroy2013-04-203-38/+15
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-2015-918/+756
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-163-9/+29
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-103-5/+8
* Finished backtracking (cf previous commit) for ARM and PowerPC.xleroy2013-03-041-41/+4
* Partial backtracking on previous commit: the "hole in Mach stack frame" xleroy2013-03-032-281/+233
* No longer a dependency on Machtypingxleroy2013-03-011-1/+0
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-015-1562/+459
* Updated ARM and PowerPC ports with new handling of __builtin_annot.xleroy2013-02-241-2/+2
* Constant propagation within __builtin_annot.xleroy2013-02-243-54/+5
* Pointers one pastxleroy2013-02-152-54/+43
* Errors for excessively large global variables or stack frames.xleroy2013-02-021-3/+2
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-296-56/+58
* Remove some useless "Require".xleroy2012-12-3010-23/+0
* Support for inline assembly (asm statements).xleroy2012-12-181-0/+4
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-8/+8