summaryrefslogtreecommitdiff
path: root/backend
Commit message (Expand)AuthorAge
* Reorganized the development, modularizing away machine-dependent parts.Gravatar xleroy2008-12-30
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.Gravatar xleroy2008-12-29
* Revised back-end so that only 2 integer registers are reserved for reloading.Gravatar xleroy2008-12-21
* Flag to turn on/off the recognition of fused multiply-add and multiply-subGravatar xleroy2008-07-31
* MAJ documentationGravatar xleroy2008-07-27
* Simplification de la semantique de LTL et LTLin. Les details lies aux conven...Gravatar xleroy2008-07-25
* Fusion partielle de la branche contsem: Gravatar xleroy2008-07-08
* Nettoyage du traitement des signatures au return dans LTL et LTLinGravatar xleroy2008-07-07
* Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs v...Gravatar xleroy2008-05-30
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...Gravatar xleroy2008-05-30
* Revu le traitement de la 'red zone' en bas de la pileGravatar xleroy2008-04-12
* Revu gestion retaddr et link dans StackingGravatar xleroy2008-04-12
* Meilleure selection pour if ((a && b) != 0), etcGravatar xleroy2008-03-27
* Nettoyages docGravatar xleroy2008-03-19
* Ajout license, README, copyright noticesGravatar xleroy2008-01-27
* Simplification des Cconst_symbol: seules les versions 'signed' sont conserveesGravatar xleroy2007-10-31
* Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFGGravatar xleroy2007-10-27
* Typo dans le pseudocode en commentaireGravatar xleroy2007-10-17
* Utilisation d'une monade avec types dependants pour garder trace des propriet...Gravatar xleroy2007-10-17
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...Gravatar xleroy2007-08-28
* Ajout de common/Complements.vGravatar xleroy2007-08-26
* DocumentationGravatar xleroy2007-08-05
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".Gravatar xleroy2007-08-04
* Importer OrderedPositive depuis Ordered.vGravatar xleroy2007-03-05
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...Gravatar xleroy2007-03-02
* Petites adaptations pour Coq 8.1gammaGravatar xleroy2006-11-11
* Lever la restriction sur les fonctions externes, restriction qui exigeait que...Gravatar xleroy2006-10-22
* Simplification de Cminor: les affectations de variables locales ne sontGravatar xleroy2006-09-18
* typo in commentGravatar xleroy2006-09-17
* Meilleure representation des worklists dans l'algo de KildallGravatar xleroy2006-09-11
* Stocker l'adresse de retour a l'offset 12 au lieu de l'offset 4 pour meilleur...Gravatar xleroy2006-09-08
* Revu traitement des variables globales dans AST.program et dans Globalenvs.Gravatar xleroy2006-09-05
* Revu la repartition des sources Coq en sous-repertoiresGravatar xleroy2006-09-04
* Fusion de la branche "traces":Gravatar xleroy2006-09-04
* Revu sémantique de Eaddrof en Csharpminor: on peut prendre l'adresse de Gravatar xleroy2006-07-11
* MAJ suite aux changements dans CminorgenGravatar xleroy2006-06-08
* Ajout Sswitch dans Csharpminor. Renommage type variable_info -> var_kindGravatar xleroy2006-06-06
* Optimisation des casts (idempotence, etc)Gravatar xleroy2006-06-05
* Ajout construction Sswitch dans CminorGravatar xleroy2006-06-05
* Ajout construction Sswitch dans CminorGravatar xleroy2006-06-05
* Revu gestion des variables globales dans CsharpminorGravatar xleroy2006-06-02
* Dans Cminor et Csharpminor: suppression de stmtlist, ajout de Sskip, Sseq.Gravatar xleroy2006-04-06
* Suppression de stmtlist et de exec_stmtlist.Gravatar xleroy2006-04-06
* PL: Un mot-cle Proof qui n'a rien a faire la...Gravatar letouzey2006-02-16
* Initial import of compcertGravatar xleroy2006-02-09