compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Add support to clightgen for generating Csyntax AST as .v files	Xavier Leroy	2021-09-22	1	-8/+0
\| \| \| \| \| \| \| \| \|	As proposed in #404. This is presented as a new option `-clight` to the existing `clightgen` tool. Revise clightgen testing to test the Csyntax output in addition to the Clight output.
*	"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".
*	Improve portability of the test for annotations inclightgen	Xavier Leroy	2020-06-05	1	-0/+2
\| \| \| \|	__builtin_ais_annot is not supported for macOS nor for Cygwin.
*	clightgen: fix the printing of annotations	Xavier Leroy	2020-06-05	1	-0/+6
	The printing of EF_annot and EF_annot_val was missing the extra "kind" parameter introduced in commit 6a010b4. Also: the automatic translation of annotations into Coq assertions was confusing and prevented other uses of __builtin_annot statements in conjunction with clightgen. I believe it was never used. This commit removes this translation. Closes: #360