compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Cminortyping: relax typechecking of function calls	Xavier Leroy	2019-06-06	1	-12/+15
\| \| \| \| \| \| \|	Sometimes the result of a void function is assigned to a variable. This can occur with C conditional expressions ?: at type void, e.g. the "assert" macro of MacOS. A similar relaxation was already there in RTLtyping.
*	Type inference and type checking for Cminor	Xavier Leroy	2019-06-06	1	-0/+797
	This module is similar to RTLtyping: it performs type inference and type checking, but on the Cminor intermediate representation rather than the RTL IR. For each function, it returns a mapping from variables to types. Its first use will be if-conversion optimization.