aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2019-07-05 15:50:26 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2019-07-05 16:57:32 +0200
commit467eb744ae2e7d913744c04866fa3e1a4558cdbe (patch)
treee38597d3f94df2184d91accd210c46a687b4ed3c /driver/Driver.ml
parentea6807fdaeaa2e46e1c7471c91056fdc4736cc2f (diff)
downloadcompcert-kvx-467eb744ae2e7d913744c04866fa3e1a4558cdbe.tar.gz
compcert-kvx-467eb744ae2e7d913744c04866fa3e1a4558cdbe.zip
Update documentation of -Obranchless
Updated man page + better usage message.
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r--driver/Driver.ml2
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]