aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Expand)AuthorAgeFilesLines
* Merge of the "princeton" branch:xleroy2013-06-163-4/+4
* powerpc: tentative support for Diab debug infoxleroy2013-05-201-24/+47
* Merge of the float32 branch: xleroy2013-05-195-28/+36
* Add option -fno-tailcalls to turn off tailcall elimination (causes problem wi...xleroy2013-05-171-2/+1
* Update PowerPC portxleroy2013-05-172-8/+14
* Preliminary support for debugging info (-g).xleroy2013-05-171-4/+70
* Refactoring: move definition of chunk_of_type to AST.v.xleroy2013-05-061-3/+0
* Stack-align to 8 arguments of Tfloat and Tlong types, as per the SVR4 ABI and...xleroy2013-05-021-16/+32
* Coq-defined equality functions for Allocation. (continued)xleroy2013-05-011-3/+10
* Updated to new CminorSelxleroy2013-04-302-3/+3
* Deactivate combination Aindexed 0 / Oadd, as it causes problems with chunk = ...xleroy2013-04-212-4/+0
* Fixes in PowerPC portxleroy2013-04-211-1/+1
* Add __builtin_bswap16 and __builtin_bswap32 to all ports.xleroy2013-04-202-2/+10
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-2015-512/+599
* Diab asm syntax issuexleroy2013-03-201-1/+1
* For Pfreeframe, generate an "addi" over GPR1 when possible, to work around a ...xleroy2013-03-181-2/+6
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-162-9/+29
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-103-5/+7
* Finished backtracking (cf previous commit) for ARM and PowerPC.xleroy2013-03-041-300/+219
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-016-2566/+1554
* Updated ARM and PowerPC ports with new handling of __builtin_annot.xleroy2013-02-243-32/+3
* Constant propagation within __builtin_annot.xleroy2013-02-241-24/+4
* Pointers one pastxleroy2013-02-151-50/+34
* Updated PowerPC port to new integers.xleroy2013-02-124-26/+49
* Errors for excessively large global variables or stack frames.xleroy2013-02-021-4/+4
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-295-31/+33
* Remove some useless "Require".xleroy2012-12-306-17/+0
* Support for inline assembly (asm statements).xleroy2012-12-181-0/+4
* Add __builtin_fcti (double -> int conversion w/ round to nearest)xleroy2012-11-242-0/+9
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-10/+13
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-062-111/+128
* Remove Val.is_true and Val.is_false, no longer used.xleroy2012-08-061-8/+2
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-235-14/+18
* Remove the PowerPC/MacOS X port, as MacOS no longer supports PowerPC.xleroy2012-07-143-926/+21
* Strip quotes from section names during #pragma parsing.xleroy2012-07-111-3/+3
* Micro-optimization of (x & mask) >>s amount into a rolm when mask >= 0.xleroy2012-07-092-16/+31
* Factor out the evaluation of the float constant in intuoffloat.xleroy2012-07-012-16/+17
* Recombine x = cmp(...); if (x == 1) ...xleroy2012-07-012-4/+57
* Added option -falign-functionsxleroy2012-07-011-4/+7
* Use Flocq for floatsxleroy2012-06-282-6/+7
* Make min_int / -1 and min_int % -1 semantically undefinedxleroy2012-06-093-5/+13
* CSE: add recognition of some combined operators, conditions, and addressing m...xleroy2012-05-265-23/+278
* Merge of the newmem branch:xleroy2012-05-213-2/+105
* Hack with nxorxleroy2012-05-182-0/+5
* checklink: first import of Valentin Robert's validator for asm and linkxleroy2012-03-281-1/+0
* PowerPC: remove the fmadd and fmsub operators/Asm instructionsxleroy2012-03-0710-62/+16
* Make CPragmas common to all ports.xleroy2012-02-272-129/+0
* Take advantage of Cmaskzero and Cmasknotzero.xleroy2012-02-242-0/+30
* Improved instruction selection for "notint".xleroy2012-02-247-11/+61
* More aggressive common subexpression elimination (CSE) of memory loads.xleroy2012-02-231-0/+55