diff options
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index eb811f6c..98eecc76 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -36,6 +36,9 @@ Require Parser. Require Initializers. Require Asmaux. +Require CSE3. +Require CSE3analysis. + (* Standard lib *) Require Import ExtrOcamlBasic. Require Import ExtrOcamlString. @@ -113,6 +116,10 @@ Extract Constant Compopts.optim_CSE => "fun _ -> !Clflags.option_fcse". Extract Constant Compopts.optim_CSE2 => "fun _ -> !Clflags.option_fcse2". +Extract Constant Compopts.optim_CSE3 => + "fun _ -> !Clflags.option_fcse3". +Extract Constant Compopts.optim_CSE3_alias_analysis => + "fun _ -> !Clflags.option_fcse3_alias_analysis". Extract Constant Compopts.optim_redundancy => "fun _ -> !Clflags.option_fredundancy". Extract Constant Compopts.optim_postpass => @@ -172,6 +179,12 @@ Extract Constant Cabs.loc => Extract Inlined Constant Cabs.string => "String.t". Extract Constant Cabs.char_code => "int64". +Extract Inlined Constant CSE3.preanalysis => "CSE3analysisaux.preanalysis". + +Extract Inductive HashedSet.PSet_internals.pset => "HashedSetaux.pset" [ "HashedSetaux.empty" "HashedSetaux.node" ] "HashedSetaux.pset_match". + +Extract Inlined Constant HashedSet.PSet_internals.pset_eq => "(==)" (* "HashedSetaux.eq" *). + (* Processor-specific extraction directives *) Load extractionMachdep. @@ -194,6 +207,7 @@ Set Extraction AccessOpaque. Cd "extraction". Separate Extraction + CSE3analysis.internal_analysis CSE3analysis.eq_depends_on_mem Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env |