aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-15 00:00:33 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-15 00:00:33 +0100
commit192d5f379b3f1efa6f12b45af36f7cfea21d6d50 (patch)
tree1c60908b258159a96ac1c55f5aef4d89f4594cae /driver/Driver.ml
parent9e706de1eb25d6d6dbeb1eb2ced71e48523a499f (diff)
downloadcompcert-kvx-192d5f379b3f1efa6f12b45af36f7cfea21d6d50.tar.gz
compcert-kvx-192d5f379b3f1efa6f12b45af36f7cfea21d6d50.zip
more inlining
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r--driver/Driver.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 43aedf50..01451e07 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -190,6 +190,7 @@ Processing options:
-Os Optimize for code size in preference to code speed
-Obranchless Optimize to generate fewer conditional branches; try to produce
branch-free instruction sequences as much as possible
+ -finline-auto-threshold n Inline functions under size n
-ftailcalls Optimize function calls in tail position [on]
-fconst-prop Perform global constant propagation [on]
-ffloat-const-prop <n> Control constant propagation of floats
@@ -322,6 +323,7 @@ let cmdline_actions =
_Regexp "-O[123]$", Unit (set_all optimization_options);
Exact "-Os", Set option_Osize;
Exact "-Obranchless", Set option_Obranchless;
+ Exact "-finline-auto-threshold", Integer (fun n -> option_inline_auto_threshold := n);
Exact "-fsmall-data", Integer(fun n -> option_small_data := n);
Exact "-fsmall-const", Integer(fun n -> option_small_const := n);
Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n);