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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-work	David Monniaux	2020-01-15	3	-24/+54
\|\
\| *	2-instruction signed division by two on Aarch64	David Monniaux	2020-01-15	3	-24/+54
\| \|
\| *	Revert "Remove `__builtin_nop` for some architectures. (#208)"	Bernhard Schommer	2020-01-03	3	-1/+8
\| \| \| \| \| \| \| \|	This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
\| *	Remove `__builtin_nop` for some architectures. (#208)	Bernhard Schommer	2019-12-21	3	-8/+1
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	The `__builtin_nop` function is documented only for PowerPC. It was added to the other architectures by copy paste, but has no known uses. So, remove `__builtin_nop` from all architectures but PowerPC.
* \|	Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work	David Monniaux	2019-12-16	1	-1/+1
\|\\|
\| *	The SP register has dwarf register number 31.	Bernhard Schommer	2019-12-11	1	-1/+1
\| \|
* \|	Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵	David Monniaux	2019-12-09	4	-5/+26
\|\\| \| \| \| \| \| \|	mppa-work-upstream-merge
\| *	Fix for AArch64 alignment problem (#206)	Bernhard Schommer	2019-11-28	3	-2/+8
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In addressing modes for load and store instructions, the offset must be a multiple of the memory size being accessed. When accessing global variables, this may not be the case if the alignment of the variable is less than its size. Errors occur at link time. This PR extends the check for a representable offset for the addressing of global variables to also check whether the variable is correctly aligned. Only if both conditions are met can we generate the short sequence Padrp / ADadr. Otherwise we go through the generic loadsymbol sequence.
\| *	Added dwarf register numbers for aarch64	Bernhard Schommer	2019-11-28	1	-3/+18
\| \|
* \|	trapping ops	David Monniaux	2019-09-24	1	-0/+30
\| \|
* \|	Merge tag 'v3.6_mppa_2019-09-20' of ↵	David Monniaux	2019-09-20	4	-7/+64
\| \| \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load
* \|	fix compiling for aarch64	David Monniaux	2019-09-20	4	-4/+42
\|/
*	Asmgenproof1: useless unfolding in proof scripts causing "omega" to fail	Xavier Leroy	2019-09-11	1	-3/+3
\| \| \| \|	"omega" fails in Coq 8.7, but not in 8.8 and later.
*	AArch64: wrong expected type for arguments of Cmaskl{zero,notzero}	xavier.leroy	2019-08-31	2	-4/+4
\| \| \| \| \| \| \| \|	The argument is of type Tlong, not Tint. This caused spurious errors in RTLtyping. Also: in AArch64/PrintOp.ml, print Cmaskl{zero,notzero} with "&l" to distinguish them from Cmask{zero,notzero}.
*	Offset out of range for ldp/stp instructions	xavier.leroy	2019-08-23	1	-1/+3
\| \| \| \|	These instructions are generated by __builtin_memcpy.
*	AArch64 port	Xavier Leroy	2019-08-08	27	-0/+14370
	This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.