compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Implement support for big endian arm targets.	Bernhard Schommer	2016-08-05	1	-0/+4
\| \| \| \| \| \| \| \|	Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418
*	configure: distinguish between ABI and processor model.	xleroy	2014-07-29	1	-1/+1
\| \| \| \| \| \| \| \|	ARM: various tweaks, incl. support for SDIV and UDIV insns when available. test/regression/funptr2.c: Thumb does weird things with <function ptr>+1. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2555 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge the various $(ARCH)/$(VARIANT)/xxx.v files into $(ARCH)/xxx.v.	xleroy	2014-07-23	1	-0/+8
\| \| \| \| \| \| \| \| \|	The only platform where we have two variants is ARM, and it's easier to share the callling convention code between the two than to maintain both variants separately. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2540 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	PowerPC/EABI port: preliminary support for #pragma section and	xleroy	2009-11-03	1	-0/+18
	#pragma use_section. Some clean-ups in Cil2Csyntax. Separate mach-dep parts of extraction/extraction.v into <arch>/extractionMachdep.v git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1167 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e