compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Flag to turn on/off the recognition of fused multiply-add and multiply-sub	xleroy	2008-07-31	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@706 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Compilo C, preprocesseur, assembleur sont determines par configure et mis ↵	xleroy	2008-04-19	1	-2/+3
\| \| \| \| \| \|	dans Makefile.config git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout du test vmach	xleroy	2008-04-15	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@612 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Problemes d'alignement des variables globales et a l'interieur de leurs ↵	xleroy	2007-10-31	1	-3/+5
\| \| \| \| \| \|	initialiseurs git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@444 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fusion des modifications faites sur les branches "tailcalls" et "smallstep".	xleroy	2007-08-04	1	-5/+4
\| \| \| \| \| \| \| \| \| \| \| \|	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
*	Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation ↵	xleroy	2007-03-02	1	-0/+5
\| \| \| \| \| \|	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
*	Ajout et utilisation de compcert_stdio.h	xleroy	2006-10-22	1	-6/+4
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@123 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Davantage de tests	xleroy	2006-09-17	1	-7/+44
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@104 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout du test lists	xleroy	2006-09-11	1	-2/+2
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@99 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	MAJ des tests C	xleroy	2006-09-08	1	-37/+11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@86 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Version C des tests Cminor	xleroy	2006-06-29	1	-0/+46
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@40 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e