debian-compcert - Debian packaging for CompCert

	Commit message (Collapse)	Author	Age
*	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
*	Ajout et utilisation de compcert_stdio.h	xleroy	2006-10-22
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@123 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Resolution d'un probleme (cf. big endian), et	blazy	2006-10-20
\| \| \| \| \| \| \| \|	mise a jour des Makefile. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@122 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout du banc de tests de CCured (Olden benchmark suite, cf.	blazy	2006-10-20
\| \| \| \| \| \| \| \| \| \|	CCured: type-safe retrofitting of legacy code, G.Necula et al.) rapportCompcert_all.txt liste les erreurs produites par ccomp. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@121 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	cleaning...	lrg	2006-10-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	interpreter for "little"	lrg	2006-10-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@119 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Meilleure compilation de la negation booleenne	xleroy	2006-09-19
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@112 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Simplification de Cminor: les affectations de variables locales ne sont	xleroy	2006-09-18
\| \| \| \| \| \| \| \|	plus des expressions mais des statements (Eassign -> Sassign). Cela simplifie les preuves et ameliore la qualite du RTL produit. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@111 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Suite des stubs variadiques.	xleroy	2006-09-17
\| \| \| \| \| \| \|	Correction bug dans Piuctf. Utiliser la 'red zone' en dessous de SP pour les conversions int<->float git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@110 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Preprocesser en definissant __ppc__ (utile pour l'emulation MacOSX/Intel)	xleroy	2006-09-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@109 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Nettoyages	xleroy	2006-09-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@108 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revu generation de stubs pour les fonctions variadiques	xleroy	2006-09-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@107 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	typo in comment	xleroy	2006-09-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@106 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Type unrolling in struct and union fields	xleroy	2006-09-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@105 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Davantage de tests	xleroy	2006-09-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@104 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Bug dans le traitement des fonctions variadiques.	xleroy	2006-09-17
\| \| \| \| \| \| \| \| \|	Tolerer les chaines litterales dans les initialiseurs. Forcer evaluation gauche-droite pour avoir les erreurs et warnings dans l'ordre du source. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@103 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Meilleur message de debug dans le cas Icall	xleroy	2006-09-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@102 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout de Init_pointer (experimental)	xleroy	2006-09-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Const.prop dans la taille des tableaux. Tolerer (avec warning) les ↵	xleroy	2006-09-16
\| \| \| \| \| \|	declarations extern ty var[]. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@100 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout du test lists	xleroy	2006-09-11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@99 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Utiliser l'extension .light.c au lieu de .clight	xleroy	2006-09-11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@98 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Typo dans impression structs	xleroy	2006-09-11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@97 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Eviter de caster les fonctions directement dans le cas variadique, gcc dit ↵	xleroy	2006-09-11
\| \| \| \| \| \|	que c'est interdit git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@96 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Suppression des casts systematiques vers unsigned int dans les comparaisons ↵	xleroy	2006-09-11
\| \| \| \| \| \|	de pointeurs git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@95 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revu traitement des structures et unions recursives. Dans Cshmgen, ↵	xleroy	2006-09-11
\| \| \| \| \| \|	meilleure compilation de exit_if_false. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@94 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Code de timing	xleroy	2006-09-11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@93 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	MAJ suite ajouts dans Kildall. Compiler en code natif par defaut	xleroy	2006-09-11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@92 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Meilleure representation des worklists dans l'algo de Kildall	xleroy	2006-09-11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@91 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e