1 files changed, 32 insertions, 0 deletions
diff --git a/driver/Compopts.v b/driver/Compopts.v
index 594b74f1..b4b9f30d 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.
 
@@ -42,8 +46,36 @@ Parameter optim_CSE2: unit -> bool.
 (** Flag -fredundancy.  For dead code elimination. *)
 Parameter optim_redundancy: unit -> bool.
 
+(** Flag -fpostpass. Postpass scheduling for K1 architecture *)
+Parameter optim_postpass: unit -> bool.
+
+(** FIXME TEMPORARY Flag -fglobaladdrtmp. Use a temporary register for loading the address of global variables (default false) *)
+Parameter optim_globaladdrtmp: unit -> bool.
+
+(** FIXME TEMPORARY Flag -fglobaladdroffset. Fold offsets into global addresses  (default false) *)
+Parameter optim_globaladdroffset: unit -> bool.
+
+(** FIXME TEMPORARY Flag -fxsaddr. Use .xs addressing mode (default true) *)
+Parameter optim_xsaddr: unit -> bool.
+
+(** FIXME TEMPORARY Flag -fcoaelesce-mem. Fuse (default true) *)
+Parameter optim_coalesce_mem: unit -> bool.
+
+(** FIXME TEMPORARY Flag -faddx. Fuse (default false) *)
+Parameter optim_addx: unit -> bool.
+
 (** Flag -fthumb.  For the ARM back-end. *)
 Parameter thumb: unit -> bool.
 
 (** Flag -g.  For insertion of debugging information. *)
 Parameter debug: unit -> bool.
+
+(** Flag -fall-loads-nontrap. Turn user loads into non trapping. *)
+Parameter all_loads_nontrap: unit -> bool.
+
+(** Flag -fforward-moves. Forward moves after CSE. *)
+Parameter optim_forward_moves: unit -> bool.
+
+(* TODO is there a more appropriate place? *)
+Require Import Coqlib.
+Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.