aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-10-31 09:58:28 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-10-31 09:58:28 +0100
commite6612fdfd69037099037def2acba5df553c3b49a (patch)
treefff8642e3d9774547de3fc83423577ebe999a902 /driver/Driver.ml
parent60e28f582b37d4080686992ea114857f75cfe6c2 (diff)
downloadcompcert-kvx-e6612fdfd69037099037def2acba5df553c3b49a.tar.gz
compcert-kvx-e6612fdfd69037099037def2acba5df553c3b49a.zip
refining CSE3 nodes
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 5d2c839f..27193ff1 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -203,6 +203,7 @@ Processing options:
-fcse3-across-merges Propagate CSE3 information across control-flow merges [on]
-fcse3-glb Refine CSE3 information using greatest lower bounds [on]
-fcse3-trivial-ops Replace trivial operations as well using CSE3 [off]
+ -fcse3-refine Refine CSE3 invariants by descending iteration [on]
-fmove-loop-invariants Perform loop-invariant code motion [off]
-fredundancy Perform redundancy elimination [on]
-fpostpass Perform postpass scheduling (only for K1 architecture) [on]
@@ -417,6 +418,7 @@ let cmdline_actions =
@ f_opt "cse3-across-merges" option_fcse3_across_merges
@ f_opt "cse3-glb" option_fcse3_glb
@ f_opt "cse3-trivial-ops" option_fcse3_trivial_ops
+ @ f_opt "cse3-refine" option_fcse3_refine
@ f_opt "move-loop-invariants" option_fmove_loop_invariants
@ f_opt "redundancy" option_fredundancy
@ f_opt "postpass" option_fpostpass