compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Cflow: analysis of "switch" was too imprecise	Xavier Leroy	2017-02-07	1	-2/+3
\| \| \| \|	Plus: updated comments.
*	Revised, more precise implementation of control-flow analysis	Xavier Leroy	2017-02-07	1	-48/+98
\| \| \| \|	The new implementation keeps track of goto labels that are actually branched to. It is less optimized than the previous implementation (no bit vectors) but perhaps easier to read.
*	Control-flow analysis: wrong flow for "case"/"default" statements	Xavier Leroy	2017-02-07	1	-4/+6
\| \| \| \|	Those labeled statements can be entered either by fall-through or by the enclosing switch.
*	More precise warnings about function returns	Xavier Leroy	2017-02-07	1	-0/+195
	This commit introduces a control-flow static analysis over C abstract syntax (file cparser/Cflow.ml) and uses it to - warn for non-void functions that can return by falling through the body - warn more precisely for _Noreturn functions that can return - introduce the "return 0" in "main" functions less often (cosmetic). For the control-flow analysis, the following conservative approximations are made: - any "goto" label is reachable - all cases of a "switch" statement are reachable as soon as the "switch" is reachable (i.e. the switch expression takes all values needed to reach every case) - the boolean expressions in "if", "while", "do"-"while" and "for" can take true and false values, unless they are compile-time constants.