diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-07-05 15:50:26 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-07-05 16:57:32 +0200 |
commit | 467eb744ae2e7d913744c04866fa3e1a4558cdbe (patch) | |
tree | e38597d3f94df2184d91accd210c46a687b4ed3c /driver | |
parent | ea6807fdaeaa2e46e1c7471c91056fdc4736cc2f (diff) | |
download | compcert-467eb744ae2e7d913744c04866fa3e1a4558cdbe.tar.gz compcert-467eb744ae2e7d913744c04866fa3e1a4558cdbe.zip |
Update documentation of -Obranchless
Updated man page + better usage message.
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Driver.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 88be8933..bd2b4cee 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -187,7 +187,7 @@ Processing options: -O0 Do not optimize the compiled code -O1 -O2 -O3 Synonymous for -O -Os Optimize for code size in preference to code speed - -Obranchless Optimize to avoid conditional branches; try to generate + -Obranchless Optimize to generate fewer conditional branches; try to produce branch-free instruction sequences as much as possible -ftailcalls Optimize function calls in tail position [on] -fconst-prop Perform global constant propagation [on] |