compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Experiment: support a subset of GCC's extended asm statements.	Xavier Leroy	2015-04-17	1	-0/+4
\|
*	Rename __builtin_cntlz to __builtin_clz.	xleroy	2014-08-27	1	-0/+4
\| \| \| \| \| \| \|	IA32: add __builtin_clz, __builtin_ctz. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2619 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fused multiply-add for IA32.	xleroy	2014-05-05	1	-0/+16
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2481 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fine hair splitting depending on whether va_list is a scalar type (IA32, ↵	xleroy	2014-01-01	1	-0/+1
\| \| \| \| \| \|	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	-1/+5
\| \| \| \| \| \|	tested on PowerPC and ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2394 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revert suppression of __builtin_{read,write}_reversed for x86 and ARM,	xleroy	2013-04-29	1	-1/+10
\| \| \| \| \| \| \| \|	for compatibility with earlier CompCert versions. But don't use them in PackedStructs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2216 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Add __builtin_bswap16 and __builtin_bswap32 to all ports.	xleroy	2013-04-20	1	-10/+5
\| \| \| \| \| \| \| \| \|	Remove __builtin_{read,write}_reversed from IA32 and ARM ports. Machregs: tighten destroyed_by_builtin Packedstructs: use bswap if read/write-reversed not available. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2208 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: first import of Valentin Robert's validator for asm and link	xleroy	2012-03-28	1	-1/+0
\| \| \| \| \| \| \|	cparser: renamed Errors to Cerrors; removed packing into Cparser. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised emulation of packed structs	xleroy	2011-10-16	1	-4/+4
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1729 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	ARM: added reversed load/store builtins + bswap builtin (to be tested)	xleroy	2011-07-30	1	-0/+3
\| \| \| \| \| \| \| \|	IA32: added bswap builtin Updated Changelog git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1693 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Nicer printing of annotations.	xleroy	2011-05-23	1	-0/+9
\| \| \| \| \| \| \|	ia32: support builtins for reversed reads and writes (facilitates testing). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1655 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Support for __builtin_fmax and __builtin_fmin	xleroy	2010-09-04	1	-0/+4
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1501 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of the reuse-temps branch:	xleroy	2010-09-02	1	-0/+28
	- Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e