compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Introduce float_conversion_default_nan parameter for float-float conversions	Bernhard Schommer	2022-04-25	1	-1/+4
\| \| \| \| \| \| \| \| \| \| \| \| \|	For RISC-V we need to return the canonical NaN value if the argument of a float32->float64 or float64->float32 conversion is any NaN. This is in line with 11.3 from the RISC-V manual, the description of the conversion operations as well as what the spike ISA simulator and qemu do. Other platforms convert the NaN payload (by truncation or expansion) in float32->float64 and float64->float32 conversions. Fixes: #428
*	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.
*	AArch64: macOS port	Xavier Leroy	2020-12-26	1	-2/+6
\| \| \| \| \|	This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors.
*	Support the use of already-installed MenhirLib and Flocq libraries	Xavier Leroy	2020-09-21	1	-2/+1
\| \| \| \|	configure flags -use-external-Flocq and -use external-MenhirLib.
*	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/+88
	This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.