aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Probleme echo -ne sur MacOS 10.5v1.2xleroy2008-03-041-0/+14
* Datesxleroy2008-01-281-1/+1
* Ajout license, README, copyright noticesxleroy2008-01-27110-4/+2027
* 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
* Ajout find_symbol_not_nullptr; nettoyagesxleroy2007-12-061-39/+71
* In Clight, revised handling of comparisons between pointers and 0xleroy2007-11-134-39/+39
* Ajout de global_addresses_distinctxleroy2007-11-031-16/+75
* Problemes d'alignement des variables globales et a l'interieur de leurs initi...xleroy2007-10-317-166/+234
* Simplification des Cconst_symbol: seules les versions 'signed' sont conserveesxleroy2007-10-311-4/+2
* Simplification des Cconst_symbol: seules les versions 'signed' sont conserveesxleroy2007-10-313-79/+59
* Revu l'heuristique de linearisationxleroy2007-10-301-46/+36
* Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFGxleroy2007-10-279-197/+363
* Typo dans le pseudocode en commentairexleroy2007-10-171-1/+1
* MAJxleroy2007-10-171-107/+107
* MAJxleroy2007-10-172-5/+6
* Relaxation de la regle d'evaluation Ecastxleroy2007-10-172-4/+4
* 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-2833-3523/+4572
* Ajout de common/Complements.vxleroy2007-08-266-2/+674
* Rendu le test lists.c plus interessantxleroy2007-08-061-4/+30
* Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefilesxleroy2007-08-0612-514/+548
* Documentationxleroy2007-08-0517-352/+584
* Deplacement du repertoire "papers" dans la hierarchie SVNxleroy2007-08-0417-6605/+0
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-04109-23374/+18742
* Version longue et mise a jour du papier sur le front-end (premier jet).blazy2007-08-0317-0/+6605
* Utilisation de Functionxleroy2007-03-231-51/+13
* Commentairesxleroy2007-03-051-4/+4
* Importer OrderedPositive depuis Ordered.vxleroy2007-03-051-30/+1
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...xleroy2007-03-0221-1010/+594
* Nettoyagexleroy2007-03-021-1/+0
* Mettre les 2 demi-espaces dans 2 blocs separesxleroy2007-03-021-9/+10
* 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-118-20/+27
* Ajout test mark&sweep GCxleroy2006-10-275-2/+439
* Ajout test stop&copy GCxleroy2006-10-263-1/+404
* Rapport d'erreur dans CILxleroy2006-10-231-1/+3
* Propagation des erreursxleroy2006-10-231-20/+94
* Relaxation des contraintes sur les struct recursivesxleroy2006-10-232-14/+10
* Location pour erreur sur le type de main()xleroy2006-10-231-1/+2
* Verification du type de retour de main()xleroy2006-10-231-10/+8
* Lever la restriction sur les fonctions externes, restriction qui exigeait que...xleroy2006-10-2219-167/+267
* Meilleur traitement des fonctions forward declared. Ajout d'un warning sur l...xleroy2006-10-221-0/+16
* Ajout et utilisation de compcert_stdio.hxleroy2006-10-226-6/+210
* Resolution d'un probleme (cf. big endian), etblazy2006-10-2011-20/+12
* Ajout du banc de tests de CCured (Olden benchmark suite, cf.blazy2006-10-20202-0/+12593
* cleaning...lrg2006-10-201-2/+1
* interpreter for "little"lrg2006-10-2016-0/+1336
generated by cgit (git 2.34.1) at 2024-05-20 09:58:50 +0000