aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selectionproof.v
Commit message (Expand)AuthorAgeFilesLines
...
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-1/+9
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-101-0/+4
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-8/+9
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-191-3/+3
* 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