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

	Commit message (Collapse)	Author	Age	Files	Lines
*	fix aarch64 merge?	Léo Gourdin	2021-03-29	1	-0/+1836
\|
*	[WIP: Coq compilation broken] Stub for Asmgen	Sylvain Boulmé	2020-06-21	1	-2138/+0
\|
*	disable leaf function removal of return address restoration due to memcpy ↵	David Monniaux	2020-03-27	1	-3/+6
\| \| \| \|	overwriting the return address register
*	Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-work	David Monniaux	2020-03-27	1	-2/+28
\|\
\| *	better epilogue proof	David Monniaux	2020-03-25	1	-8/+18
\| \|
\| *	removed RA restoration	David Monniaux	2020-03-25	1	-1/+17
\| \|
* \|	Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-work	David Monniaux	2020-03-26	1	-187/+436
\|\\|
\| *	RA is preserved	David Monniaux	2020-03-25	1	-12/+20
\| \|
\| *	Asmgenproof1	David Monniaux	2020-03-24	1	-1/+3
\| \|
\| *	transl_addressing_correct	David Monniaux	2020-03-24	1	-4/+9
\| \|
\| *	transl_op_correct	David Monniaux	2020-03-24	1	-10/+14
\| \|
\| *	transl_cond	David Monniaux	2020-03-24	1	-143/+332
\| \|
\| *	progress in proofs about RA	David Monniaux	2020-03-24	1	-16/+57
\| \|
* \|	Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-work	David Monniaux	2020-01-15	1	-14/+38
\|\ \
\| * \|	2-instruction signed division by two on Aarch64	David Monniaux	2020-01-15	1	-14/+38
\| \|/
* \|	Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵	David Monniaux	2019-12-09	1	-1/+1
\|\\| \| \| \| \| \| \|	mppa-work-upstream-merge
\| *	Fix for AArch64 alignment problem (#206)	Bernhard Schommer	2019-11-28	1	-1/+1
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
* \|	Merge tag 'v3.6_mppa_2019-09-20' of ↵	David Monniaux	2019-09-20	1	-1/+1
\|/ \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load
*	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 port	Xavier Leroy	2019-08-08	1	-0/+1836
	This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.