compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Improved semantics of casts	xleroy	2011-07-17	1	-9/+8
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1685 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to ↵	xleroy	2011-07-16	1	-63/+40
\| \| \| \| \| \| \| \| \|	the type of the whole conditional expression. Replaced predicates "cast", "is_true" and "is_false" by functions "sem_cast" and "bool_val". git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1684 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of branch "unsigned-offsets":	xleroy	2011-04-09	1	-2/+3
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	- In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Incompatibility 8.3 / 8.3pl1	xleroy	2011-03-14	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1606 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Slightly nicer semantics for initialization	xleroy	2011-03-13	1	-28/+29
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1604 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	More global initialization work done and proved in Coq.	xleroy	2011-03-13	1	-12/+312
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1603 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Initializers for global variables: compile-time evaluation of expressions ↵	xleroy	2011-03-12	1	-0/+555
	done in Coq (module Initializers), using the same primitives as those for CompCert C's semantics. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1602 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e