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 /cparser/Checks.mli | |
| parent | c0eb337aff9fe81733b15fceb79d92f7d52f1dfd (diff) | |
| download | compcert-kvx-80872f3f92e513817cb7f9396a757cf0db95c2c7.tar.gz compcert-kvx-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'.
Diffstat (limited to 'cparser/Checks.mli')
0 files changed, 0 insertions, 0 deletions