compcert-kvx - Unnamed repository; edit this file 'description' to name the repository.

	Commit message (Collapse)	Author	Age	Files	Lines
*	k1c -> kvx changes	David Monniaux	2020-05-26	1	-1/+1
\|
*	Restored previous input sizes for other backends	Cyril SIX	2019-09-25	1	-0/+4
\|
*	Reducing further the input size of the tests	Cyril SIX	2019-09-13	1	-1/+1
\|
*	Starting to modify official CompCert tests to be passable with the simu	Cyril SIX	2019-09-10	1	-1/+1
\|
*	Reduce the running times of the tests in test/c	Xavier Leroy	2017-08-26	1	-1/+1
\| \| \| \|	Running times were too long when executed on low-end ARM or PowerPC hardware, or under QEMU emulation.
*	Updates to the local test suite	Xavier Leroy	2016-07-24	1	-17/+19
\| \| \| \| \| \| \|	- Adjust parameters to bring the running time of each test closer to 1 second - compression/arcode.c: array access one past - "inline" -> "static inline" - Remove cchecklink support
*	Merge of "newspilling" branch:	xleroy	2014-07-23	1	-6/+6
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- 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
*	Merge of the float32 branch:	xleroy	2013-05-19	1	-0/+196
	- added RTL type "Tsingle" - ABI-compatible passing of single-precision floats on ARM and x86 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e