summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Revu removeproofGravatar xleroy2008-03-19
* Nettoyages docGravatar xleroy2008-03-19
* Probleme echo -ne sur MacOS 10.5Gravatar xleroy2008-03-04
* DatesGravatar xleroy2008-01-28
* Ajout license, README, copyright noticesGravatar xleroy2008-01-27
* Function -> Definition (probleme de performance avec Coq8.1pl3)Gravatar xleroy2008-01-07
* Ajout corollaires et overlap pour le papier JAR (pas encore utilises dans Com...Gravatar xleroy2007-12-08
* Ajout find_symbol_not_nullptr; nettoyagesGravatar xleroy2007-12-06
* In Clight, revised handling of comparisons between pointers and 0Gravatar xleroy2007-11-13
* Ajout de global_addresses_distinctGravatar xleroy2007-11-03
* Problemes d'alignement des variables globales et a l'interieur de leurs initi...Gravatar xleroy2007-10-31
* Simplification des Cconst_symbol: seules les versions 'signed' sont conserveesGravatar xleroy2007-10-31
* Simplification des Cconst_symbol: seules les versions 'signed' sont conserveesGravatar xleroy2007-10-31
* Revu l'heuristique de linearisationGravatar xleroy2007-10-30
* Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFGGravatar xleroy2007-10-27
* Typo dans le pseudocode en commentaireGravatar xleroy2007-10-17
* MAJGravatar xleroy2007-10-17
* MAJGravatar xleroy2007-10-17
* Relaxation de la regle d'evaluation EcastGravatar 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
* Rendu le test lists.c plus interessantGravatar xleroy2007-08-06
* Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu MakefilesGravatar xleroy2007-08-06
* DocumentationGravatar xleroy2007-08-05
* Deplacement du repertoire "papers" dans la hierarchie SVNGravatar xleroy2007-08-04
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".Gravatar xleroy2007-08-04
* Version longue et mise a jour du papier sur le front-end (premier jet).Gravatar blazy2007-08-03
* Utilisation de FunctionGravatar xleroy2007-03-23
* CommentairesGravatar xleroy2007-03-05
* 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
* NettoyageGravatar xleroy2007-03-02
* Mettre les 2 demi-espaces dans 2 blocs separesGravatar xleroy2007-03-02
* Preuve des 2 axiomes restantsGravatar xleroy2007-03-02
* Ajout lemmes utiles sur egalite decidableGravatar xleroy2007-03-02
* Ajout operation eq dans PMap et IndexedMapGravatar xleroy2007-01-03
* Petites adaptations pour Coq 8.1gammaGravatar xleroy2006-11-11
* Ajout test mark&sweep GCGravatar xleroy2006-10-27
* Ajout test stop&copy GCGravatar xleroy2006-10-26
* Rapport d'erreur dans CILGravatar xleroy2006-10-23
* Propagation des erreursGravatar xleroy2006-10-23
* Relaxation des contraintes sur les struct recursivesGravatar xleroy2006-10-23
* Location pour erreur sur le type de main()Gravatar xleroy2006-10-23
* Verification du type de retour de main()Gravatar xleroy2006-10-23
* Lever la restriction sur les fonctions externes, restriction qui exigeait que...Gravatar xleroy2006-10-22
* Meilleur traitement des fonctions forward declared. Ajout d'un warning sur l...Gravatar xleroy2006-10-22
* Ajout et utilisation de compcert_stdio.hGravatar xleroy2006-10-22
* Resolution d'un probleme (cf. big endian), etGravatar blazy2006-10-20
* Ajout du banc de tests de CCured (Olden benchmark suite, cf.Gravatar blazy2006-10-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 13:29:13 +0000