From 893827f54addca2facc19a8f342b380d63114130 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 27 Jan 2020 11:43:00 +0100 Subject: Added a flag to desactivate tail duplication --- driver/Compopts.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'driver/Compopts.v') 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. -- cgit