compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Extended inline asm: handle missing cases.	Xavier Leroy	2015-04-28	1	-1/+7
\| \| \| \| \| \|	Bitfields: better translation of initializers and compound literals; run this pass before unblocking. Transform.stmt: extend with ability to treat unblocked code. test/regression: more bitfield tests.
*	ABI compatibility for struct/union function arguments passed by value.	Xavier Leroy	2015-01-27	1	-1/+1
\| \| \| \| \| \| \| \| \| \|	The passing of struct/union arguments by value implemented in the verified part of CompCert is not compatible with the ARM, PowerPC and x86 ABI. Here we enrich the StructReturn source-to-source emulation pass so that it implements the calling conventions defined in these ABIs. Plus: for x86, implement the returning of struct/union results by value in a way compatible with the ABI.
*	PR#10 continued: disambiguate record to avoid OCaml warning	Xavier Leroy	2014-12-30	1	-1/+1
\|
*	PR#10: composite definitions must be maintained in the environment.	Xavier Leroy	2014-12-30	1	-6/+15
\|
*	Support C99 compound literals (by expansion in Unblock pass).	xleroy	2014-08-21	1	-26/+175
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	C: Support array initializers that are too short + default init for remainder.	xleroy	2014-03-28	1	-10/+14
\| \| \| \| \| \| \| \|	Elab: Handle C99 designated initializers. C2C, Initializers: more precise intermediate AST for initializers. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2439 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Support for inline assembly (asm statements).	xleroy	2012-12-18	1	-0/+1
\| \| \| \| \| \| \|	cparser: add primitive support for enum types. bitfield emulation: for bitfields with enum type, choose signed/unsigned as appropriate git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2074 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: first import of Valentin Robert's validator for asm and link	xleroy	2012-03-28	1	-1/+1
\| \| \| \| \| \| \|	cparser: renamed Errors to Cerrors; removed packing into Cparser. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Switching to the new C parser/elaborator/simplifier	xleroy	2010-03-03	1	-0/+133
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e