compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Upgrade embedded version of Flocq to 3.1.	Guillaume Melquiond	2019-03-27	1	-11/+14
\| \| \| \| \| \| \| \| \| \| \| \|	Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully).
*	Hybrid 64bit/32bit PowerPC port	Bernhard Schommer	2017-05-03	1	-6/+6
\| \| \| \| \| \| \| \| \| \| \| \| \|	This commit adds code generation for 64bit PowerPC architectures which execute 32bit applications. The main difference to the normal 32bit PowerPC port is that it uses the available 64bit instructions instead of using the runtime library functions. However pointers are still 32bit and the 32bit calling convention is used. In order to use this port the target architecture must be either in Server execution mode or if in Embedded execution mode the high order 32 bits of GPRs must be implemented in 32-bit mode. Furthermore the operating system must preserve the high order 32 bits of GPRs.
*	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