aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Expand)AuthorAgeFilesLines
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-191-21/+17
* Added support for jump tables in back end.xleroy2009-11-101-12/+131
* Support Clight initializers of the form "int * x = &y;".xleroy2009-11-012-0/+5
* No '\n' in Coq strings...xleroy2009-08-181-2/+2
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-163-60/+790
* Added 'going wrong' behaviorsxleroy2009-08-051-11/+34
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-058-107/+107
* Added tail call optimization passxleroy2009-03-262-0/+26
* Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >...xleroy2009-02-261-0/+17
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-61/+173
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-302-956/+0
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.xleroy2008-12-292-50/+50
* Fusion partielle de la branche contsem: xleroy2008-07-082-56/+125
* Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs v...xleroy2008-05-301-0/+24
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...xleroy2008-05-302-0/+352
* Amelioration compilation des switchxleroy2008-04-171-30/+70
* Ajout license, README, copyright noticesxleroy2008-01-2710-0/+145
* Ajout find_symbol_not_nullptr; nettoyagesxleroy2007-12-061-39/+71
* Ajout de global_addresses_distinctxleroy2007-11-031-16/+75
* Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFGxleroy2007-10-271-4/+4
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-284-30/+98
* Ajout de common/Complements.vxleroy2007-08-263-1/+669
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-049-2089/+3426
* Ajout de Init_pointer (experimental)xleroy2006-09-172-2/+8
* Revu traitement des variables globales dans AST.program et dans Globalenvs.xleroy2006-09-053-314/+445
* Revu la repartition des sources Coq en sous-repertoiresxleroy2006-09-046-0/+4580
generated by cgit (git 2.34.1) at 2024-06-03 02:58:33 +0000