debian-compcert - Debian packaging for CompCert

	Commit message (Collapse)	Author	Age
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	Traiter les initialisations x = NULL	xleroy	2006-09-08
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@89 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Suite de l'adaptation du front-end CIL	xleroy	2006-09-08
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@87 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Integration du front-end CIL developpe par Thomas Moniot	xleroy	2006-09-07
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@84 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	MAJ	xleroy	2006-09-06
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@79 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Definition redondante	xleroy	2006-09-06
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@78 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fusion de la branche "traces":	xleroy	2006-09-04
\| \| \| \| \| \| \| \| \| \| \| \| \|	- Ajout de traces d'evenements d'E/S dans les semantiques - Ajout constructions switch et allocation dynamique - Initialisation des variables globales - Portage Coq 8.1 beta Debut d'integration du front-end C: - Traduction Clight -> Csharpminor dans cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout d'un type-checker (non certifie) pour Cminor	xleroy	2006-07-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@51 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Declaration des variables avec .comm	xleroy	2006-07-11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@50 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Suppression de stmtlist dans Cminor	xleroy	2006-04-06
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@12 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Renommage List -> CList lors de l'extraction	xleroy	2006-03-09
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@8 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Initial import of compcert	xleroy	2006-02-09
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e