aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Added tail call optimization passxleroy2009-03-263-6/+847
* New linearization heuristicxleroy2009-02-271-32/+72
* Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive f...xleroy2009-01-294-10/+6
* Elimination of "alloc" instruction in Caml files and test files.xleroy2009-01-115-24/+0
* - Added alignment constraints to memory loads and stores.xleroy2009-01-1138-537/+137
* Fixed unary minusxleroy2009-01-071-1/+1
* Cminor, CminorSel: removed useless premises in rules for Sreturnxleroy2009-01-042-4/+0
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-3032-11274/+2075
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.xleroy2008-12-298-44/+49
* Revised back-end so that only 2 integer registers are reserved for reloading.xleroy2008-12-2119-402/+780
* Flag to turn on/off the recognition of fused multiply-add and multiply-subxleroy2008-07-312-20/+29
* MAJ documentationxleroy2008-07-276-361/+110
* Simplification de la semantique de LTL et LTLin. Les details lies aux conven...xleroy2008-07-258-523/+538
* Fusion partielle de la branche contsem: xleroy2008-07-088-1732/+1652
* Nettoyage du traitement des signatures au return dans LTL et LTLinxleroy2008-07-076-107/+96
* Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs v...xleroy2008-05-303-52/+77
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...xleroy2008-05-308-4/+55
* Revu le traitement de la 'red zone' en bas de la pilexleroy2008-04-128-58/+65
* Revu gestion retaddr et link dans Stackingxleroy2008-04-1217-934/+1032
* Meilleure selection pour if ((a && b) != 0), etcxleroy2008-03-272-27/+277
* Nettoyages docxleroy2008-03-192-15/+6
* 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