aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selectionproof.v
Commit message (Expand)AuthorAgeFilesLines
...
* Forgot to add some filesxleroy2009-08-181-0/+505
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-1398/+0
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.xleroy2008-12-291-8/+12
* Revised back-end so that only 2 integer registers are reserved for reloading.xleroy2008-12-211-1/+1
* Flag to turn on/off the recognition of fused multiply-add and multiply-subxleroy2008-07-311-6/+9
* Fusion partielle de la branche contsem: xleroy2008-07-081-129/+136
* Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs v...xleroy2008-05-301-15/+32
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...xleroy2008-05-301-0/+1
* Meilleure selection pour if ((a && b) != 0), etcxleroy2008-03-271-20/+191
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-281-581/+524
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-0/+1240