From a15858a0a8fcea82db02fe8c9bd2ed912210419f Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 18 Aug 2010 09:06:55 +0000 Subject: Merge of branches/full-expr-4: - Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/extraction.v | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 797204f..706d1db 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -75,6 +75,17 @@ Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring". (* Linearize *) Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux". +(* Compiler *) +Extract Constant Compiler.print_Csyntax => "PrintCsyntax.print_if". +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_castopt => "PrintRTL.print_castopt". +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". + (* Suppression of stupidly big equality functions *) Extract Constant Op.eq_operation => "fun (x: operation) (y: operation) -> x = y". Extract Constant Op.eq_addressing => "fun (x: addressing) (y: addressing) -> x = y". -- cgit v1.2.3