aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Ajout license, README, copyright noticesxleroy2008-01-2755-0/+663
* Simplification des Cconst_symbol: seules les versions 'signed' sont conserveesxleroy2007-10-313-79/+59
* Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFGxleroy2007-10-273-158/+257
* Typo dans le pseudocode en commentairexleroy2007-10-171-1/+1
* Utilisation d'une monade avec types dependants pour garder trace des propriet...xleroy2007-10-173-556/+461
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-287-1407/+1739
* Ajout de common/Complements.vxleroy2007-08-261-0/+3
* Documentationxleroy2007-08-056-119/+126
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-0455-10999/+12921
* Importer OrderedPositive depuis Ordered.vxleroy2007-03-051-30/+1
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...xleroy2007-03-029-156/+185
* Petites adaptations pour Coq 8.1gammaxleroy2006-11-111-1/+0
* Lever la restriction sur les fonctions externes, restriction qui exigeait que...xleroy2006-10-2216-141/+209
* Simplification de Cminor: les affectations de variables locales ne sontxleroy2006-09-186-880/+689
* typo in commentxleroy2006-09-171-1/+1
* Meilleure representation des worklists dans l'algo de Kildallxleroy2006-09-114-68/+209
* Stocker l'adresse de retour a l'offset 12 au lieu de l'offset 4 pour meilleur...xleroy2006-09-088-19/+19
* Revu traitement des variables globales dans AST.program et dans Globalenvs.xleroy2006-09-0511-18/+18
* Revu la repartition des sources Coq en sous-repertoiresxleroy2006-09-049-8171/+0
* Fusion de la branche "traces":xleroy2006-09-0453-8018/+4666
* Revu sémantique de Eaddrof en Csharpminor: on peut prendre l'adresse de xleroy2006-07-113-165/+149
* MAJ suite aux changements dans Cminorgenxleroy2006-06-081-3/+7
* Ajout Sswitch dans Csharpminor. Renommage type variable_info -> var_kindxleroy2006-06-063-27/+61
* Optimisation des casts (idempotence, etc)xleroy2006-06-052-51/+121
* Ajout construction Sswitch dans Cminorxleroy2006-06-051-8/+39
* Ajout construction Sswitch dans Cminorxleroy2006-06-053-9/+103
* Revu gestion des variables globales dans Csharpminorxleroy2006-06-023-274/+457
* Dans Cminor et Csharpminor: suppression de stmtlist, ajout de Sskip, Sseq.xleroy2006-04-069-349/+247
* Suppression de stmtlist et de exec_stmtlist.xleroy2006-04-061-45/+31
* PL: Un mot-cle Proof qui n'a rien a faire la...letouzey2006-02-161-1/+0
* Initial import of compcertxleroy2006-02-0955-0/+40577