debian-compcert - Debian packaging for CompCert

	Commit message (Collapse)	Author	Age
*	Revu le traitement de la 'red zone' en bas de la pile	xleroy	2008-04-12
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@605 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revu gestion retaddr et link dans Stacking	xleroy	2008-04-12
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@604 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Meilleure selection pour if ((a && b) != 0), etc	xleroy	2008-03-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@581 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revu removeproof	xleroy	2008-03-19
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@567 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Nettoyages doc	xleroy	2008-03-19
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@566 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Probleme echo -ne sur MacOS 10.5	xleroy	2008-03-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@548 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Dates	xleroy	2008-01-28
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@491 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout license, README, copyright notices	xleroy	2008-01-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Function -> Definition (probleme de performance avec Coq8.1pl3)	xleroy	2008-01-07
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@470 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout corollaires et overlap pour le papier JAR (pas encore utilises dans ↵	xleroy	2007-12-08
\| \| \| \| \| \|	Compcert) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@460 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout find_symbol_not_nullptr; nettoyages	xleroy	2007-12-06
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@455 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	In Clight, revised handling of comparisons between pointers and 0	xleroy	2007-11-13
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@447 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout de global_addresses_distinct	xleroy	2007-11-03
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@445 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Problemes d'alignement des variables globales et a l'interieur de leurs ↵	xleroy	2007-10-31
\| \| \| \| \| \|	initialiseurs git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@444 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Simplification des Cconst_symbol: seules les versions 'signed' sont conservees	xleroy	2007-10-31
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@443 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Simplification des Cconst_symbol: seules les versions 'signed' sont conservees	xleroy	2007-10-31
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@442 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revu l'heuristique de linearisation	xleroy	2007-10-30
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@438 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFG	xleroy	2007-10-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@437 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Typo dans le pseudocode en commentaire	xleroy	2007-10-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@423 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	MAJ	xleroy	2007-10-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@422 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	MAJ	xleroy	2007-10-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@421 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Relaxation de la regle d'evaluation Ecast	xleroy	2007-10-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@420 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Utilisation d'une monade avec types dependants pour garder trace des ↵	xleroy	2007-10-17
\| \| \| \| \| \|	proprietes state_incr git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@419 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les ↵	xleroy	2007-08-28
\| \| \| \| \| \|	expressions sont maintenant pures et les appels de fonctions sont des statements. Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor. Preuve de preservation semantique pour les programmes qui divergent. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout de common/Complements.v	xleroy	2007-08-26
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@405 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Rendu le test lists.c plus interessant	xleroy	2007-08-06
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@388 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefiles	xleroy	2007-08-06
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@387 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Documentation	xleroy	2007-08-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Deplacement du repertoire "papers" dans la hierarchie SVN	xleroy	2007-08-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@385 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fusion des modifications faites sur les branches "tailcalls" et "smallstep".	xleroy	2007-08-04
\| \| \| \| \| \| \| \| \| \| \| \|	En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Version longue et mise a jour du papier sur le front-end (premier jet).	blazy	2007-08-03
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@383 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Utilisation de Function	xleroy	2007-03-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@210 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Commentaires	xleroy	2007-03-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@184 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Importer OrderedPositive depuis Ordered.v	xleroy	2007-03-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@183 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation ↵	xleroy	2007-03-02
\| \| \| \| \| \|	de Lattice pour utiliser une notion d'egalite possiblement differente de =. Adaptation de Kildall et de ses utilisateurs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Nettoyage	xleroy	2007-03-02
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@181 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Mettre les 2 demi-espaces dans 2 blocs separes	xleroy	2007-03-02
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@180 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Preuve des 2 axiomes restants	xleroy	2007-03-02
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@179 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout lemmes utiles sur egalite decidable	xleroy	2007-03-02
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@178 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout operation eq dans PMap et IndexedMap	xleroy	2007-01-03
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@158 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Petites adaptations pour Coq 8.1gamma	xleroy	2006-11-11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@135 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout test mark&sweep GC	xleroy	2006-10-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@134 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout test stop&copy GC	xleroy	2006-10-26
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@133 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Rapport d'erreur dans CIL	xleroy	2006-10-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@130 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Propagation des erreurs	xleroy	2006-10-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Relaxation des contraintes sur les struct recursives	xleroy	2006-10-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@128 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Location pour erreur sur le type de main()	xleroy	2006-10-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@127 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Verification du type de retour de main()	xleroy	2006-10-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Lever la restriction sur les fonctions externes, restriction qui exigeait ↵	xleroy	2006-10-22
\| \| \| \| \| \|	que tous les arguments resident en registres git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Meilleur traitement des fonctions forward declared. Ajout d'un warning sur ↵	xleroy	2006-10-22
\| \| \| \| \| \|	le nombre d'arguments d'une fonction externe, qui est actuellement limite par le back-end git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@124 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e