compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Fusion des modifications faites sur les branches "tailcalls" et "smallstep".	xleroy	2007-08-04	55	-10999/+12921
\| \| \| \| \| \| \| \| \| \| \| \|	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
*	Importer OrderedPositive depuis Ordered.v	xleroy	2007-03-05	1	-30/+1
\| \| \| \|	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	9	-156/+185
\| \| \| \| \| \|	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
*	Petites adaptations pour Coq 8.1gamma	xleroy	2006-11-11	1	-1/+0
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@135 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Lever la restriction sur les fonctions externes, restriction qui exigeait ↵	xleroy	2006-10-22	16	-141/+209
\| \| \| \| \| \|	que tous les arguments resident en registres git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Simplification de Cminor: les affectations de variables locales ne sont	xleroy	2006-09-18	6	-880/+689
\| \| \| \| \| \| \| \|	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
*	typo in comment	xleroy	2006-09-17	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@106 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Meilleure representation des worklists dans l'algo de Kildall	xleroy	2006-09-11	4	-68/+209
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@91 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Stocker l'adresse de retour a l'offset 12 au lieu de l'offset 4 pour ↵	xleroy	2006-09-08	8	-19/+19
\| \| \| \| \| \|	meilleure compatibilite avec les conventions de MacOSX git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@85 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revu traitement des variables globales dans AST.program et dans Globalenvs.	xleroy	2006-09-05	11	-18/+18
\| \| \| \| \| \| \| \|	Adaptation frontend, backend en consequence. Integration passe C -> C#minor dans common/Main.v. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@77 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revu la repartition des sources Coq en sous-repertoires	xleroy	2006-09-04	9	-8171/+0
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@73 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fusion de la branche "traces":	xleroy	2006-09-04	53	-8018/+4666
\| \| \| \| \| \| \| \| \| \| \| \| \|	- 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
*	Revu sémantique de Eaddrof en Csharpminor: on peut prendre l'adresse de	xleroy	2006-07-11	3	-165/+149
\| \| \| \| \| \| \| \| \|	globaux qui ne sont pas déclarés dans les variables du programme, notamment les fonctions. Adaptation de Cminorgen et de sa preuve en conséquence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@47 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	MAJ suite aux changements dans Cminorgen	xleroy	2006-06-08	1	-3/+7
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@36 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout Sswitch dans Csharpminor. Renommage type variable_info -> var_kind	xleroy	2006-06-06	3	-27/+61
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@35 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Optimisation des casts (idempotence, etc)	xleroy	2006-06-05	2	-51/+121
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@33 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout construction Sswitch dans Cminor	xleroy	2006-06-05	1	-8/+39
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@32 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout construction Sswitch dans Cminor	xleroy	2006-06-05	3	-9/+103
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@31 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revu gestion des variables globales dans Csharpminor	xleroy	2006-06-02	3	-274/+457
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@30 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Dans Cminor et Csharpminor: suppression de stmtlist, ajout de Sskip, Sseq.	xleroy	2006-04-06	9	-349/+247
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@11 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Suppression de stmtlist et de exec_stmtlist.	xleroy	2006-04-06	1	-45/+31
\| \| \| \| \| \| \| \|	Ajout de Sskip, Sseq. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@10 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	PL: Un mot-cle Proof qui n'a rien a faire la...	letouzey	2006-02-16	1	-1/+0
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@5 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Initial import of compcert	xleroy	2006-02-09	55	-0/+40577
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e