compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Improve portability of the test for annotations inclightgen	Xavier Leroy	2020-06-05	2	-0/+4
\| \| \| \|	__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
*	clightgen: sanitize names of functions and global variables	Xavier Leroy	2019-10-28	1	-0/+12
\| \| \| \| \|	A "dollar" sign in a function name or a global variable name was producing incorrect Coq identifiers. (Issue #319.)
*	Clean .foo.aux files created by coqc	Xavier Leroy	2018-07-10	1	-1/+1
\|
*	Don't depend on ../../clightgen	Xavier Leroy	2018-06-02	1	-3/+3
\| \| \| \| \|	It's not really necessary, and under Windows it's really ../../clightgen.exe, which confuses make.
*	Add tests for clightgen	Xavier Leroy	2018-06-01	4	-0/+977
	Also: add "parallel" entry to test/Makefile for parallel execution of tests.