compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	- Recognize __builtin_fabs as an operator, not just a builtin,	xleroy	2013-11-06	1	-1/+11
\| \| \| \| \| \| \| \| \|	enabling more aggressive optimizations. - Less aggressive CSE for EF_builtin builtins, causes problems for __builtin_write{16,32}_reversed. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2363 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised handling of int->float conversions:	xleroy	2013-07-08	1	-5/+7
\| \| \| \| \| \| \| \| \| \|	- introduce Float.floatofint{,u} and use it in the semantics of C - prove that it is equivalent to int->double conversion followed by double->float rounding, and use this fact to justify code generation in Cshmgen. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2294 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Treat casts int64 -> float32 as primitive operations instead of two	xleroy	2013-07-03	1	-5/+7
\| \| \| \| \| \| \| \|	casts int64 -> float64 -> float32. The latter causes double rounding errors. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2290 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of the "princeton" branch:	xleroy	2013-06-16	1	-3/+3
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Define type "block" as "positive" instead of "Z". - Strengthen mem_unchanged_on so that the permissions are identical, instead of possibly increasing. - Move mem_unchanged_on from Events to Memory.Mem. - Define it in terms of mem_contents rather than in terms of Mem.load. - ExportClight: try to name temporaries introduced by SimplExpr - SimplExpr: avoid reusing temporaries between different functions, instead, thread a single generator through all functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised semantics and compilation of 2-argument C operators to better match	xleroy	2013-05-06	1	-93/+67
\| \| \| \| \| \| \| \|	"the usual binary conversions" and be more robust towards future extensions e.g. with 32-bit float values. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2239 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	driver: removed option -flonglong	xleroy	2013-04-22	1	-25/+34
\| \| \| \| \| \| \| \|	test/c: added SHA3 cfrontend: support casts between long long and pointers, and comparisons between them. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2213 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20	1	-310/+643
\| \| \| \| \| \| \| \| \|	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
*	Pointers one past	xleroy	2013-02-15	1	-14/+15
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Make Clight independent of CompCert C.	xleroy	2012-10-08	1	-0/+822
	Common parts are factored out in cfrontend/Ctypes.v and cfrontend/Cop.v git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2060 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e