From 5a7fc8637ae82d9aaf71c0053078a950ddee3b89 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 7 Feb 2017 09:57:45 +0100 Subject: More precise warnings about function returns 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. --- cparser/Cutil.mli | 5 ----- 1 file changed, 5 deletions(-) (limited to 'cparser/Cutil.mli') diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 4eaa9e4a..bd5a2c3e 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -285,8 +285,3 @@ val subst_expr: exp IdentMap.t -> exp -> exp val subst_init: exp IdentMap.t -> init -> init val subst_decl: exp IdentMap.t -> decl -> decl val subst_stmt: exp IdentMap.t -> stmt -> stmt - -(* Statement properties *) - -val contains_return: stmt -> bool - (* Does the stmt contain a return. *) -- cgit