aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Asmgenproof1.v
Commit message (Expand)AuthorAgeFilesLines
...
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-1/+1
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-191-7/+7
* Simplified the treatment of the PowerPC small data area; now more specific to...xleroy2009-11-021-98/+72
* Preliminary support for small data area in PowerPC port.xleroy2009-11-011-33/+65
* Storing of single floats: must insert frsp instruction before store. (Tempor...xleroy2009-10-301-11/+26
* Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >...xleroy2009-02-261-5/+29
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-29/+4
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-0/+1632