compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Merge of branch seq-and-or. See Changelog for details.	xleroy	2012-10-06	1	-5/+0
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	- Revised non-overflow constraints on memory injections so that	xleroy	2012-07-23	1	-0/+1
\| \| \| \| \| \| \| \| \| \|	injections compose (Values, Memdata, Memory) - Memory chunks: Mfloat64 now has alignment 8; introduced Mfloat64al32 that works like old Mfloat64 (i.e. has alignment 4); simplified handling of memcpy builtin accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1983 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Use Flocq for floats	xleroy	2012-06-28	1	-3/+3
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Another update from Andrew Tolmach	xleroy	2012-03-09	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1840 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	PrintCminor: printing Sskip	xleroy	2012-03-09	1	-1/+1
\| \| \| \| \| \| \|	test/cminor: updating git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1839 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of Andrew Tolmach's HASP-related changes	xleroy	2012-03-09	1	-6/+41
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1838 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of the "volatile" branch:	xleroy	2012-02-04	1	-0/+11
\| \| \| \| \| \| \| \| \| \| \| \|	- native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express \|\| and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml chars	xleroy	2011-10-18	1	-2/+2
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of branches/full-expr-4:	xleroy	2010-08-18	1	-0/+285
	- Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e