From 17f519651feb4a09aa90c89c949469e8a5ab0e88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 17 Aug 2014 07:52:12 +0000 Subject: - Support "switch" statements over 64-bit integers (in CompCert C to Cminor, included) - Translation of "switch" to decision trees or jumptables made generic over the sizes of integers and moved to the Cminor->CminorSel pass instead of CminorSel->RTL as before. - CminorSel: add "exitexpr" to support the above. - ValueDomain: more precise analysis of comparisons against an integer literal. E.g. "x >=u 0" is always true. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2565 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/extraction.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index d987629..a097bdb 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -16,6 +16,7 @@ Require AST. Require Iteration. Require Floats. Require SelectLong. +Require Selection. Require RTLgen. Require Inlining. Require ValueDomain. @@ -62,9 +63,9 @@ Extract Constant SelectLong.get_helper => Extract Constant SelectLong.get_builtin => "fun s sg -> Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))". +Extract Constant Selection.compile_switch => "Switchaux.compile_switch". (* RTLgen *) -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. @@ -133,7 +134,7 @@ Load extractionMachdep. (* Avoid name clashes *) Extraction Blacklist List String Int. -(* Cutting the dependancy to R. *) +(* Cutting the dependency to R. *) Extract Inlined Constant Fcore_defs.F2R => "fun _ -> assert false". Extract Inlined Constant Fappli_IEEE.FF2R => "fun _ -> assert false". Extract Inlined Constant Fappli_IEEE.B2R => "fun _ -> assert false". -- cgit v1.2.3