compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Support Clight initializers of the form "int * x = &y;".	xleroy	2009-11-01	1	-0/+9
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1162 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Problem with const enum initializers	xleroy	2009-09-15	2	-0/+4
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1146 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Stronger constant folding, esp. w.r.t. floats	xleroy	2009-08-21	2	-0/+7
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1137 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Cil2Csyntax: added goto and labels; added assignment between structs	xleroy	2009-08-16	1	-0/+6
\| \| \| \| \| \| \| \| \| \| \| \|	Kildall: simplified the interface Constprop, CSE, Allocation, Linearize: updated for the new Kildall RTL, LTL: removed the well-formedness condition on the CFG, it is no longer necessary with the new Kildall and it is problematic for validated optimizations. Maps: more efficient implementation of PTree.fold. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1124 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Elimination of "alloc" instruction in Caml files and test files.	xleroy	2009-01-11	1	-2/+4
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@946 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Test for int/float conversions	xleroy	2009-01-07	3	-1/+140
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@943 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Endianness in tests	xleroy	2009-01-05	4	-2/+20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Continuation of PowerPC/EABI port	xleroy	2008-12-31	2	-2/+2
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@933 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout nouveaux tests	xleroy	2008-08-09	52	-0/+8446
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@708 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	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
*	Update test results	xleroy	2008-07-31	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@704 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Augmenter le temps d'execution par defaut	xleroy	2008-07-25	2	-2/+2
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@700 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Compilo C, preprocesseur, assembleur sont determines par configure et mis ↵	xleroy	2008-04-19	2	-5/+8
\| \| \| \| \| \|	dans Makefile.config git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Amelioration compilation des switch	xleroy	2008-04-17	1	-0/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@616 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout du test vmach	xleroy	2008-04-15	3	-1/+219
\| \| \| \|	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	3	-3/+53
\| \| \| \| \| \|	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	2	-2/+5
\| \| \| \| \| \|	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
*	Rendu le test lists.c plus interessant	xleroy	2007-08-06	1	-4/+30
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@388 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefiles	xleroy	2007-08-06	5	-226/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@387 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Documentation	xleroy	2007-08-05	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fusion des modifications faites sur les branches "tailcalls" et "smallstep".	xleroy	2007-08-04	8	-19/+38
\| \| \| \| \| \| \| \| \| \| \| \|	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
*	Nettoyage	xleroy	2007-03-02	1	-1/+0
\| \| \| \|	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	1	-9/+10
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@180 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout test mark&sweep GC	xleroy	2006-10-27	5	-2/+439
\| \| \| \|	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	3	-1/+404
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@133 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout et utilisation de compcert_stdio.h	xleroy	2006-10-22	6	-6/+210
\| \| \| \|	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	10	-19/+11
\| \| \| \| \| \| \| \|	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	202	-0/+12593
\| \| \| \| \| \| \| \| \| \|	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	1	-2/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	interpreter for "little"	lrg	2006-10-20	16	-0/+1336
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@119 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Simplification de Cminor: les affectations de variables locales ne sont	xleroy	2006-09-18	1	-5/+10
\| \| \| \| \| \| \| \|	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
*	Nettoyages	xleroy	2006-09-17	4	-18/+16
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@108 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Davantage de tests	xleroy	2006-09-17	33	-33/+3010
\| \| \| \|	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	2	-2/+57
\| \| \| \|	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	8	-61/+1082
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@86 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Integration du front-end CIL developpe par Thomas Moniot	xleroy	2006-09-07	1	-78/+62
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@84 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fusion de la branche "traces":	xleroy	2006-09-04	6	-26/+113
\| \| \| \| \| \| \| \| \| \| \| \| \|	- 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 de fabs	xleroy	2006-07-11	1	-0/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@49 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Cast des litteraux de chaine en unsigned char *	xleroy	2006-07-11	2	-12/+12
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@48 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Version C des tests Cminor	xleroy	2006-06-29	8	-0/+1339
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@40 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Initial import of compcert	xleroy	2006-02-09	18	-0/+2224
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e