diff options
Diffstat (limited to 'extraction/extraction.v')
| -rw-r--r-- | extraction/extraction.v | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 521c0cdd..5a1ca0be 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -34,6 +34,11 @@ Require Clight. Require Compiler. Require Parser. Require Initializers. +<<<<<<< HEAD +Require Int31. +Require Asmaux. +======= +>>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf (* Standard lib *) Require Import ExtrOcamlBasic. @@ -110,10 +115,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". @@ -176,7 +193,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. |