Merge of the newmem branch:

- Revised memory model with Max and Cur permissions, but without bounds
- Constant propagation of 'const' globals
- Function inlining at RTL level
- (Unprovable) elimination of unreferenced static definitions


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 17 insertions, 2 deletions

diff --git a/extraction/extraction.v b/extraction/extraction.v
index 4861ff9..1156d04 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -10,9 +10,12 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+Require Wfsimpl.
 Require Iteration.
 Require Floats.
 Require RTLgen.
+Require Inlining.
+Require Constprop.
 Require Coloring.
 Require Allocation.
 Require Compiler.
@@ -22,6 +25,9 @@ Require Initializers.
 Require Import ExtrOcamlBasic.
 Require Import ExtrOcamlString.
 
+(* Wfsimpl *)
+Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm.
+
 (* Float *)
 Extract Inlined Constant Floats.float => "float".
 Extract Constant Floats.Float.zero   => "0.".
@@ -53,8 +59,6 @@ Extraction NoInline Memory.Mem.valid_pointer.
 Extraction Inline Errors.bind Errors.bind2.
 
 (* Iteration *)
-Extract Constant Iteration.dependent_description' =>
-  "fun x -> assert false".
 
 Extract Constant Iteration.GenIter.iterate =>
   "let rec iter f a =
@@ -66,9 +70,19 @@ Extract Constant RTLgen.compile_switch => "RTLgenaux.compile_switch".
 Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely".
 Extraction Inline RTLgen.ret RTLgen.error RTLgen.bind RTLgen.bind2.
 
+(* Inlining *)
+Extract Inlined Constant Inlining.should_inline => "Inliningaux.should_inline".
+Extraction Inline Inlining.ret Inlining.bind.
+
 (* RTLtyping *)
 Extract Constant RTLtyping.infer_type_environment => "RTLtypingaux.infer_type_environment".
 
+(* Constprop *)
+Extract Constant ConstpropOp.propagate_float_constants =>
+  "fun _ -> !Clflags.option_ffloatconstprop >= 1".
+Extract Constant Constprop.generate_float_constants =>
+  "fun _ -> !Clflags.option_ffloatconstprop >= 2".
+
 (* Coloring *)
 Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring".
 
@@ -83,6 +97,7 @@ Extract Constant Compiler.print_Clight => "PrintClight.print_if".
 Extract Constant Compiler.print_Cminor => "PrintCminor.print_if".
 Extract Constant Compiler.print_RTL => "PrintRTL.print_rtl".
 Extract Constant Compiler.print_RTL_tailcall => "PrintRTL.print_tailcall".
+Extract Constant Compiler.print_RTL_inline => "PrintRTL.print_inlining".
 Extract Constant Compiler.print_RTL_constprop => "PrintRTL.print_constprop".
 Extract Constant Compiler.print_RTL_cse => "PrintRTL.print_cse".
 Extract Constant Compiler.print_LTLin => "PrintLTLin.print_if".