compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Wrong syntax in fcmp.	Xavier Leroy	2015-09-13	1	-2/+2
\|
*	PowerPC 64 bits: alternate, more efficient implementations of int64 operations.	Xavier Leroy	2015-09-12	12	-0/+677
\|
*	Support va_arg for vararg arguments of composite (struct/union) types.	Xavier Leroy	2015-03-20	1	-0/+7
\| \| \| \|	Now for IA32 and PowerPC as well.
*	stdarg.h: assorted fixes for PowerPC	xleroy	2014-01-01	1	-5/+5
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2397 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fine hair splitting depending on whether va_list is a scalar type (IA32, ↵	xleroy	2014-01-01	1	-3/+3
\| \| \| \| \| \|	ARM) or an array type (PowerPC). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2395 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Experimental support for <stdarg.h>, the GCC way. Works on IA32. To be ↵	xleroy	2014-01-01	1	-0/+156
\| \| \| \| \| \|	tested on PowerPC and ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2394 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	powerpc: faster implementation of long division modeled on that for IA32	xleroy	2013-07-03	4	-68/+218
\| \| \| \| \| \| \| \|	test: add one test (2^64-1) / (2^32+3) to exercise a special case of this long division. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2288 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Wrong pseudo-instr	xleroy	2013-05-06	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2236 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Support for in64 -> float conversions w/ correct rounding.	xleroy	2013-05-06	2	-0/+132
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2235 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	ia32/i64_dtou: wrong play on rounding mode	xleroy	2013-05-05	2	-10/+36
\| \| \| \| \| \| \| \| \|	arm, powerpc: expand shifts inline in dtos and dtou arm: branchless code for shl and shr test: more tests for double -> long long conversions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2234 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Typos in comments	xleroy	2013-04-30	2	-3/+3
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2220 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Expand 64-bit integer comparisons into 32-bit integer comparisons.	xleroy	2013-04-29	2	-144/+0
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2218 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fixes in PowerPC port	xleroy	2013-04-21	6	-61/+108
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2209 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Split arch/int64.s into one file per function.	xleroy	2013-04-20	14	-442/+911
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2206 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Remove __i64_{neg,add,sub,mul}, now handled directly by the compiler.	xleroy	2013-04-20	1	-50/+0
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2204 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20	1	-0/+492
	1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e