aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Cshmgenproof3.v
Commit message (Expand)AuthorAgeFilesLines
* Merge of branches/full-expr-4:xleroy2010-08-181-1667/+0
* Support for inlined built-ins.xleroy2010-06-291-4/+11
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-11/+13
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-101-0/+1
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-119/+75
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-161-4/+15
* Added 'going wrong' behaviorsxleroy2009-08-051-6/+7
* Transition semantics for Clight and Csharpminorxleroy2009-08-031-1052/+869
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-107/+108
* Clight: ajout Econdition, suppression Eindex.xleroy2008-09-271-17/+37
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
* Relaxation de la regle d'evaluation Ecastxleroy2007-10-171-2/+2
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-281-517/+840
* Documentationxleroy2007-08-051-10/+42
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-98/+81
* Revu traitement des structures et unions recursives. Dans Cshmgen, meilleure...xleroy2006-09-111-16/+10
* Csem: l'hypothese de typage sur main est inutile (assuree par wt_program)xleroy2006-09-061-5/+12
* Revu traitement des variables globales dans AST.program et dans Globalenvs.xleroy2006-09-051-30/+27
* Fusion de la branche "traces":xleroy2006-09-041-0/+1503
generated by cgit (git 2.34.1) at 2024-06-28 23:51:23 +0000