aboutsummaryrefslogtreecommitdiffstats
path: root/backend/PPCgenproof1.v
Commit message (Expand)AuthorAgeFilesLines
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-1686/+0
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.xleroy2008-12-291-7/+8
* Revised back-end so that only 2 integer registers are reserved for reloading.xleroy2008-12-211-57/+57
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...xleroy2008-05-301-0/+5
* Revu le traitement de la 'red zone' en bas de la pilexleroy2008-04-121-5/+5
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
* Simplification des Cconst_symbol: seules les versions 'signed' sont conserveesxleroy2007-10-311-32/+25
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-39/+19
* Lever la restriction sur les fonctions externes, restriction qui exigeait que...xleroy2006-10-221-40/+57
* Fusion de la branche "traces":xleroy2006-09-041-0/+112
* Initial import of compcertxleroy2006-02-091-0/+1566