From 80872f3f92e513817cb7f9396a757cf0db95c2c7 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 17 Feb 2017 13:51:01 +0100 Subject: Do not optimize away the 'return 0' at end of 'main' As a cosmetic optimization enabled by the static analysis in Cflow, we used to not insert a 'return 0' at end of 'main' if the body of 'main' cannot fall through. Since this optimization is cosmetic (the back-end will remove the 'return 0' if unused) and since we don't fully trust this static analysis, revert this optimization and always insert 'return 0'. --- cparser/Elab.ml | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) (limited to 'cparser') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index eb9ff560..02980529 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2336,13 +2336,11 @@ let elab_fundef env spec name defs body loc = if s = "main" then begin match unroll env ty_ret with | TInt(IInt, []) -> - (* Add implicit "return 0;" at end of function body, unless - this control point is unreachable, e.g. function already - returns in all cases. *) - if can_fallthrough then - sseq no_loc body1 - {sdesc = Sreturn(Some(intconst 0L IInt)); sloc = no_loc} - else body1 + (* Add implicit "return 0;" at end of function body. + If we trusted the return analysis, we would do this only if + this control point is reachable, i.e if can_fallthrough is true. *) + sseq no_loc body1 + {sdesc = Sreturn(Some(intconst 0L IInt)); sloc = no_loc} | _ -> warning loc Main_return_type "return type of 'main' should be 'int'"; body1 -- cgit