compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	- Added alignment constraints to memory loads and stores.	xleroy	2009-01-11	11	-367/+162
\| \| \| \| \| \| \| \| \| \| \|	- In Cminor and below, removed pointer validity check in semantics of comparisons, so that evaluation of expressions is independent of memory state. - In Cminor and below, removed "alloc" instruction. - Cleaned up commented-away parts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Cminor, CminorSel: removed useless premises in rules for Sreturn	xleroy	2009-01-04	1	-2/+2
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@938 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Continuation of ARM port.	xleroy	2009-01-01	1	-1/+1
\| \| \| \| \| \| \|	Cleaned up Makefile and SVN properties. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@935 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Cleanup	xleroy	2008-12-31	1	-105/+0
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@934 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Continuation of PowerPC/EABI port	xleroy	2008-12-31	2	-147/+373
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@933 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Reorganized the development, modularizing away machine-dependent parts.	xleroy	2008-12-30	17	-0/+12583
	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