compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Improve error messages.	Bernhard Schommer	2018-03-07	1	-0/+5
\| \| \| \| \| \| \| \|	Include the format specifier in error message when available in order to make it easier to spot the broken ais parameter. Futhermore introduce a new warning for unused ais parameters. Bug 22464
*	Reactivated and improved ais annotations.	Bernhard Schommer	2018-03-06	1	-1/+7
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The ais annotations are now handled in a separate file shared between all architectures. Also two different variants of replacements are supported, %e which expands to ais expressions and %l which also expands to an ais expression but is guaranted to be usable as l-value in the ais annotation. Otherwise the new warning is Wrong_is_parameter is generated. Also an error message is generated if floating point variables are used in ais annotations since a3 does not support them at the moment. Additionally an error message is generated for plain volatile variables used, since they will enforce a volatile load and result in the value being passed to the annotation instead of the address as other global variables.
*	Added error summary in case of fatal error.	Bernhard Schommer	2018-02-09	1	-0/+10
\|
*	Refactor the handling of errors and warnings (#44)	Bernhard Schommer	2018-02-08	1	-0/+437
	* Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/ * Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the Diagnostics module. * Raise on error before calling external tools. * Added diagnostics to clightgen. * Fix error handling of AsmToJson. * Cleanup error handling of Elab and C2C. *The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.