aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2014-11-16 18:39:43 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2014-11-16 18:39:43 +0100
commitbda5ee25ac991c38f5541a234936f1f6e2226072 (patch)
treec26b8de4fac8a9e747f73a08adf25707786619fd /extraction
parentef4334c5b3984277a0844ba94f6b3945152e3637 (diff)
downloadcompcert-kvx-bda5ee25ac991c38f5541a234936f1f6e2226072.tar.gz
compcert-kvx-bda5ee25ac991c38f5541a234936f1f6e2226072.zip
Add flags to control individual optimization passes + flag -O0 for turning them off.
Diffstat (limited to 'extraction')
-rw-r--r--extraction/extraction.v8
1 files changed, 7 insertions, 1 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 5b71a150..ee496ffa 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -92,8 +92,14 @@ Extract Constant Compopts.propagate_float_constants =>
"fun _ -> !Clflags.option_ffloatconstprop >= 1".
Extract Constant Compopts.generate_float_constants =>
"fun _ -> !Clflags.option_ffloatconstprop >= 2".
-Extract Constant Compopts.eliminate_tailcalls =>
+Extract Constant Compopts.optim_tailcalls =>
"fun _ -> !Clflags.option_ftailcalls".
+Extract Constant Compopts.optim_constprop =>
+ "fun _ -> !Clflags.option_fconstprop".
+Extract Constant Compopts.optim_CSE =>
+ "fun _ -> !Clflags.option_fcse".
+Extract Constant Compopts.optim_redundancy =>
+ "fun _ -> !Clflags.option_fredundancy".
Extract Constant Compopts.thumb =>
"fun _ -> !Clflags.option_mthumb".