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 /lib/Json.ml | |
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'.
Diffstat (limited to 'lib/Json.ml')
0 files changed, 0 insertions, 0 deletions