aboutsummaryrefslogtreecommitdiffstats
path: root/backend/RTLtyping.v
Commit message (Expand)AuthorAgeFilesLines
* Support for inlined built-ins.xleroy2010-06-291-4/+26
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-22/+14
* More realistic treatment of jump tables: show the absence of overflow when ac...xleroy2009-11-101-2/+4
* Added support for jump tables in back end.xleroy2009-11-101-0/+14
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-161-1/+1
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-161-7/+6
* Added tail call optimization passxleroy2009-03-261-6/+0
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-18/+1
* Revu gestion retaddr et link dans Stackingxleroy2008-04-121-3/+2
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-133/+223
* Lever la restriction sur les fonctions externes, restriction qui exigeait que...xleroy2006-10-221-19/+0
* Revu traitement des variables globales dans AST.program et dans Globalenvs.xleroy2006-09-051-2/+2
* Fusion de la branche "traces":xleroy2006-09-041-1003/+227
* Initial import of compcertxleroy2006-02-091-0/+1277