aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Constprop.v
Commit message (Expand)AuthorAgeFilesLines
* Refactoring of Constprop and Constpropproof into a machine-dependent part and...xleroy2009-08-171-1078/+0
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-161-17/+2
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-6/+6
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-2/+2
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-0/+1093