aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Cshmgenproof2.v
Commit message (Expand)AuthorAgeFilesLines
* Utilisation de intoffloatu. Ajout du cas int + ptr.xleroy2008-05-311-1/+5
* Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs v...xleroy2008-05-301-4/+4
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
* In Clight, revised handling of comparisons between pointers and 0xleroy2007-11-131-6/+15
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-281-92/+90
* Documentationxleroy2007-08-051-2/+2
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-62/+41
* Meilleure compilation de la negation booleennexleroy2006-09-191-6/+0
* Permettre les casts entre types de fonctionxleroy2006-09-061-1/+5
* Fusion de la branche "traces":xleroy2006-09-041-0/+419