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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Merge branch 'master' into merge_master_8.13.1	Sylvain Boulmé	2021-03-23	1	-4/+4
\|\ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
\| *	Replace `omega` tactic with `lia`	Xavier Leroy	2020-12-29	1	-4/+4
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
* \|	Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3	David Monniaux	2020-12-02	1	-98/+81
\|\ \
\| * \|	op_valid_pointer_eq for aarch64	David Monniaux	2020-10-19	1	-0/+14
\| \| \|
\| * \|	non trapping op	David Monniaux	2020-09-30	1	-64/+49
\| \| \|
\| * \|	non trapping	David Monniaux	2020-09-30	1	-2/+0
\| \| \|
\| * \|	AArch64 division no longer "traps"	David Monniaux	2020-09-30	1	-32/+32
\| \| \|
* \| \|	cond_valid_pointer_eq	David Monniaux	2020-11-25	1	-5/+13
\| \| \|
* \| \|	pointer_eq copied	David Monniaux	2020-11-25	1	-0/+14
\|/ /
* \|	adapting new stuff for ARM and AArch64	David Monniaux	2020-04-01	1	-3/+8
\| \|
* \|	trapping ops	David Monniaux	2019-09-24	1	-0/+30
\| \|
* \|	Merge tag 'v3.6_mppa_2019-09-20' of ↵	David Monniaux	2019-09-20	1	-0/+40
\|/ \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load
*	AArch64: wrong expected type for arguments of Cmaskl{zero,notzero}	xavier.leroy	2019-08-31	1	-2/+2
\| \| \| \| \| \| \| \|	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}.
*	AArch64 port	Xavier Leroy	2019-08-08	1	-0/+1778
	This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.