diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-12 17:22:46 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-12 17:22:46 +0100 |
commit | 8f337598016aa49ff6554085b406b7e6026bfc3d (patch) | |
tree | 16337be33b8a5c8897191c1f1e651b807099aa01 /driver | |
parent | 0e6e9bd0f68c5f628510603221463ed6b9fa2d54 (diff) | |
download | compcert-kvx-8f337598016aa49ff6554085b406b7e6026bfc3d.tar.gz compcert-kvx-8f337598016aa49ff6554085b406b7e6026bfc3d.zip |
-fpostpass-ilp
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Clflags.ml | 1 | ||||
-rw-r--r-- | driver/Driver.ml | 2 |
2 files changed, 3 insertions, 0 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 77fae8ee..4d70d350 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -28,6 +28,7 @@ let option_fconstprop = ref true let option_fcse = ref true let option_fredundancy = ref true let option_fpostpass = ref true +let option_fpostpass_ilp = ref false let option_falignfunctions = ref (None: int option) let option_falignbranchtargets = ref 0 let option_faligncondbranchs = ref 0 diff --git a/driver/Driver.ml b/driver/Driver.ml index 467cf989..c68c066a 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -194,6 +194,7 @@ Processing options: -fcse Perform common subexpression elimination [on] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] + -fpostpass-ilp Use integer linear programming for postpass scheduling [off] -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their single caller [on] @@ -363,6 +364,7 @@ let cmdline_actions = @ f_opt "cse" option_fcse @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass + @ f_opt "postpass-ilp" option_fpostpass_ilp @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once (* Code generation options *) |