diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-17 13:51:01 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-17 13:51:01 +0100 |
commit | 80872f3f92e513817cb7f9396a757cf0db95c2c7 (patch) | |
tree | 74b7f3fdc19c11fe79ff1db6024501ef534a280b | |
parent | c0eb337aff9fe81733b15fceb79d92f7d52f1dfd (diff) | |
download | compcert-80872f3f92e513817cb7f9396a757cf0db95c2c7.tar.gz compcert-80872f3f92e513817cb7f9396a757cf0db95c2c7.zip |
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'.
-rw-r--r-- | cparser/Elab.ml | 12 |
1 files changed, 5 insertions, 7 deletions
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 |