aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Expand)AuthorAgeFilesLines
* Coloringaux: make identifiers unique; special treatment of precolored xleroy2009-08-263-65/+129
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-162-4/+35
* Unionfind data structure, used in new implementation of backend/Tunnelingxleroy2009-08-161-0/+702
* Added 'going wrong' behaviorsxleroy2009-08-052-0/+120
* Use Extraction Blacklistxleroy2009-07-251-4/+4
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-059-235/+239
* Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >...xleroy2009-02-261-0/+20
* Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive f...xleroy2009-01-291-5/+4
* - Added alignment constraints to memory loads and stores.xleroy2009-01-112-53/+25
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-302-0/+169
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.xleroy2008-12-292-258/+724
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...xleroy2008-05-301-0/+1
* Suppression de 'exten', inutilisexleroy2008-05-301-6/+0
* Ajout license, README, copyright noticesxleroy2008-01-279-0/+125
* Function -> Definition (probleme de performance avec Coq8.1pl3)xleroy2008-01-071-1/+1
* Ajout corollaires et overlap pour le papier JAR (pas encore utilises dans Com...xleroy2007-12-081-6/+363
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-043-242/+367
* Utilisation de Functionxleroy2007-03-231-51/+13
* Commentairesxleroy2007-03-051-4/+4
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...xleroy2007-03-024-706/+248
* Preuve des 2 axiomes restantsxleroy2007-03-021-2/+17
* Ajout lemmes utiles sur egalite decidablexleroy2007-03-021-0/+31
* Ajout operation eq dans PMap et IndexedMapxleroy2007-01-031-0/+10
* Petites adaptations pour Coq 8.1gammaxleroy2006-11-115-16/+25
* Lever la restriction sur les fonctions externes, restriction qui exigeait que...xleroy2006-10-221-1/+43
* Fusion de la branche "traces":xleroy2006-09-047-165/+1705
* Initial import of compcertxleroy2006-02-099-0/+5563
generated by cgit (git 2.34.1) at 2024-06-02 20:17:08 +0000