aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Cminorgen.v
Commit message (Collapse)AuthorAgeFilesLines
* Revu sémantique de Eaddrof en Csharpminor: on peut prendre l'adresse de xleroy2006-07-111-24/+23
| | | | | | | | | globaux qui ne sont pas déclarés dans les variables du programme, notamment les fonctions. Adaptation de Cminorgen et de sa preuve en conséquence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@47 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout Sswitch dans Csharpminor. Renommage type variable_info -> var_kindxleroy2006-06-061-5/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@35 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu gestion des variables globales dans Csharpminorxleroy2006-06-021-34/+60
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@30 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Dans Cminor et Csharpminor: suppression de stmtlist, ajout de Sskip, Sseq.xleroy2006-04-061-34/+26
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@11 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Initial import of compcertxleroy2006-02-091-0/+398
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e