compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Support for 64-bit architectures: update the PowerPC port	Xavier Leroy	2016-10-01	1	-3/+12
\| \| \| \| \|	The PowerPC port remains 32-bit only, no support is added for PPC 64. This shows how much work is needed to update an existing port a minima.
*	Port to Coq 8.5pl2	Xavier Leroy	2016-07-08	1	-3/+2
\| \| \| \| \|	Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
*	bug 17392: remove trailing whitespace in source files	Michael Schmidt	2015-10-14	1	-2/+2
\|
*	Use PowerPC 64 bits instructions (when available) for int<->FP conversions.	Xavier Leroy	2015-09-13	1	-0/+4
\| \| \| \| \| \|	Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence. Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-".
*	The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM.	xleroy	2014-07-28	1	-1/+4
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2550 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of "newspilling" branch:	xleroy	2014-07-23	1	-3/+11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	PowerPC is big-endian, dammit.	xleroy	2014-02-21	1	-2/+2
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2412 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Introduce and use the platform-specific Archi module giving:	xleroy	2014-01-03	1	-0/+34
	- endianness - alignment constraints for 8-byte types (which is 4 for x86 ABI and 8 for other ABIs) - NaN handling options (superceding the Nan module, removed). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2402 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e