compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Add a test for int64 -> float32 conversion	Xavier Leroy	2020-03-30	1	-1/+2
\| \| \| \| \|	This is a special value that causes double rounding with the naive conversion schema int64 -> float64 -> float32.
*	Turn 64-bit integer division and modulus by constants into multiply-high	Xavier Leroy	2016-10-04	1	-0/+12
\| \| \| \| \| \|	This trick was already implemented for 32-bit integer division and modulus. Here we extend it to the 64-bit case. For 32-bit target processors, the runtime library must implement 64-bit multiply-high (signed and unsigned). Tentative implementations are provided for IA32 and PowerPC, but need testing.
*	Treat casts int64 -> float32 as primitive operations instead of two	xleroy	2013-07-03	1	-0/+5
\| \| \| \| \| \| \| \|	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
*	Follow-up to commit 2288: add test for special case of long division.	xleroy	2013-07-03	1	-1/+2
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2289 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Interp.ml: support printf of long long	xleroy	2013-04-20	1	-2/+4
\| \| \| \| \| \| \|	test/regression: add test "int32"; update test "int64" git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2201 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20	1	-0/+115
	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