aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Cshmgenproof2.v
Commit message (Expand)AuthorAgeFilesLines
* Suppressed axioms Float.eq_zero_{true,false}, since the latter isxleroy2010-05-091-8/+4
* Add "fabs" (floating-point absolute value) as a unary operator inxleroy2010-05-021-0/+13
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-1/+1
* Function types didn't always degrade to pointers like they should. Introduce...xleroy2010-03-021-1/+1
* Transition semantics for Clight and Csharpminorxleroy2009-08-031-72/+38
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-2/+2
* 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