diff options
Diffstat (limited to 'extraction/extraction.v')
| -rw-r--r-- | extraction/extraction.v | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index c0286f7b..265a5967 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -35,6 +35,7 @@ Require Compiler. Require Parser. Require Initializers. Require Int31. +Require Asmaux. (* Standard lib *) Require Import ExtrOcamlBasic. @@ -111,10 +112,22 @@ Extract Constant Compopts.optim_CSE => "fun _ -> !Clflags.option_fcse". Extract Constant Compopts.optim_redundancy => "fun _ -> !Clflags.option_fredundancy". +Extract Constant Compopts.optim_postpass => + "fun _ -> !Clflags.option_fpostpass". Extract Constant Compopts.thumb => "fun _ -> !Clflags.option_mthumb". Extract Constant Compopts.debug => "fun _ -> !Clflags.option_g". +Extract Constant Compopts.optim_globaladdrtmp => + "fun _ -> !Clflags.option_fglobaladdrtmp". +Extract Constant Compopts.optim_globaladdroffset => + "fun _ -> !Clflags.option_fglobaladdroffset". +Extract Constant Compopts.optim_xsaddr => + "fun _ -> !Clflags.option_fxsaddr". +Extract Constant Compopts.optim_addx => + "fun _ -> !Clflags.option_faddx". +Extract Constant Compopts.optim_coalesce_mem => + "fun _ -> !Clflags.option_fcoalesce_mem". (* Compiler *) Extract Constant Compiler.print_Clight => "PrintClight.print_if". @@ -185,7 +198,8 @@ Separate Extraction Machregs.mregs_for_operation Machregs.mregs_for_builtin Machregs.two_address_op Machregs.is_stack_reg Machregs.destroyed_at_indirect_call - AST.signature_main + AST.signature_main Asmaux Floats.Float32.from_parsed Floats.Float.from_parsed Globalenvs.Senv.invert_symbol - Parser.translation_unit_file. + Parser.translation_unit_file + Compopts.optim_postpass. |