aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Compopts.v
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2020-01-27 11:43:00 +0100
committerCyril SIX <cyril.six@kalray.eu>2020-01-27 11:43:00 +0100
commit893827f54addca2facc19a8f342b380d63114130 (patch)
treea6dd12cc5313a996d94806b5c6711f27ef361064 /driver/Compopts.v
parent8aa9cb8c221ad4f2d27a7c54eca256bc70425aff (diff)
downloadcompcert-kvx-893827f54addca2facc19a8f342b380d63114130.tar.gz
compcert-kvx-893827f54addca2facc19a8f342b380d63114130.zip
Added a flag to desactivate tail duplication
Diffstat (limited to 'driver/Compopts.v')
-rw-r--r--driver/Compopts.v4
1 files changed, 4 insertions, 0 deletions
diff --git a/driver/Compopts.v b/driver/Compopts.v
index fdd2b1d6..a979c69b 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -27,6 +27,10 @@ Parameter generate_float_constants: unit -> bool.
(** For value analysis. Currently always false. *)
Parameter va_strict: unit -> bool.
+(** Flag -fduplicate. For tail duplication optimization. Necessary to have
+ * bigger superblocks *)
+Parameter optim_duplicate: unit -> bool.
+
(** Flag -ftailcalls. For tail call optimization. *)
Parameter optim_tailcalls: unit -> bool.