compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Updated the Caml part. Added some more tests in annot1.c.	Xavier Leroy	2015-03-27	1	-0/+36
\|
*	Constant propagation within __builtin_annot.	xleroy	2013-02-24	1	-0/+9
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Coloringaux: better cost estimate for annotation builtins	xleroy	2011-06-14	1	-3/+39
\| \| \| \| \| \| \|	Regression: more tests for annotations git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1675 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised handling of annotation statements, and more generally built-in ↵	xleroy	2011-06-13	1	-8/+9
\| \| \| \| \| \|	functions, and more generally external functions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Adding __builtin_annotation	xleroy	2010-09-01	1	-0/+23
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e