compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Use the LGPL instead of the GPL for dual-licensed files	Xavier Leroy	2021-05-08	1	-4/+5
\| \| \| \| \| \|	The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate.
*	"macosx" is now called "macos"	Xavier Leroy	2021-01-18	1	-1/+1
\| \| \| \| \|	The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos".
*	AArch64: macOS port	Xavier Leroy	2020-12-26	1	-7/+19
\| \| \| \| \|	This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors.
*	Move declarations of __builtin_clz* and __builtin_ctz* to C2C.ml	Xavier Leroy	2020-07-27	1	-8/+0
\| \| \| \|	These functions are now available on all targets.
*	Dual-license aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v}	Xavier Leroy	2020-05-05	1	-0/+3
\| \| \| \| \| \|	The corresponding files in all other ports are dual-licensed (GPL + non-commercial), there is no reason it should be different for aarch64.
*	AArch64 port	Xavier Leroy	2019-08-08	1	-0/+72
	This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.