aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Ctyping.v
Commit message (Expand)AuthorAgeFilesLines
* Add a type system for CompCert C and type-checking constructor functions.Xavier Leroy2014-12-311-0/+1999
* Merge of branches/full-expr-4:xleroy2010-08-181-459/+0
* Support for inlined built-ins.xleroy2010-06-291-6/+12
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-3/+3
* Transition semantics for Clight and Csharpminorxleroy2009-08-031-0/+7
* Clight: ajout Econdition, suppression Eindex.xleroy2008-09-271-4/+4
* 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-49/+47
* Documentationxleroy2007-08-051-3/+9
* Revu traitement des structures et unions recursives. Dans Cshmgen, meilleure...xleroy2006-09-111-4/+9
* Csem: l'hypothese de typage sur main est inutile (assuree par wt_program)xleroy2006-09-061-4/+9
* Revu traitement des variables globales dans AST.program et dans Globalenvs.xleroy2006-09-051-4/+4
* Fusion de la branche "traces":xleroy2006-09-041-0/+420