compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	More interoperability tests.	Xavier Leroy	2015-01-28	1	-4/+8
\|
*	ABI compatibility for struct/union function arguments passed by value.	Xavier Leroy	2015-01-27	1	-0/+62
	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.