compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Reorganized the development, modularizing away machine-dependent parts.	xleroy	2008-12-30	1	-501/+0
\| \| \| \| \| \| \| \| \|	Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Extract Coq lists to Caml lists.	xleroy	2008-12-29	1	-19/+19
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@929 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Clight: ajout Econdition, suppression Eindex.	xleroy	2008-09-27	1	-4/+11
\| \| \| \| \| \| \| \|	caml/PrintCsyntax.ml: afficher les formes a[b] et a->fld. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@789 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Impression des 'for'	xleroy	2008-04-19	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@620 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout license, README, copyright notices	xleroy	2008-01-27	1	-0/+15
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Problemes d'alignement des variables globales et a l'interieur de leurs ↵	xleroy	2007-10-31	1	-1/+1
\| \| \| \| \| \|	initialiseurs git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@444 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les ↵	xleroy	2007-08-28	1	-17/+26
\| \| \| \| \| \|	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
*	Relaxation des contraintes sur les struct recursives	xleroy	2006-10-23	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@128 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout de Init_pointer (experimental)	xleroy	2006-09-17	1	-0/+32
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Typo dans impression structs	xleroy	2006-09-11	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@97 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revu traitement des structures et unions recursives. Dans Cshmgen, ↵	xleroy	2006-09-11	1	-32/+28
\| \| \| \| \| \|	meilleure compilation de exit_if_false. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@94 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Suite de l'adaptation du front-end CIL	xleroy	2006-09-08	1	-22/+30
\| \| \| \|	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	1	-0/+434
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@84 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e