diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-03 20:09:19 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-03 20:11:48 +0200 |
| commit | 677771949bd62f7f5bbcf99bba6b6f816f07a6c2 (patch) | |
| tree | 597b2ccc5867bc2bbb083c4e13f792671b2042c1 /extraction | |
| parent | 36e64ee96ded0c94c83da6fb12202c276e66ba45 (diff) | |
| parent | b7e0d70de2ace6f0a22f9f65cc244d875ee48496 (diff) | |
| download | compcert-kvx-677771949bd62f7f5bbcf99bba6b6f816f07a6c2.tar.gz compcert-kvx-677771949bd62f7f5bbcf99bba6b6f816f07a6c2.zip | |
Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-if-conversion
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index e2ffd65d..265a5967 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -73,6 +73,7 @@ Extract Constant Iteration.GenIter.iterate => (* Selection *) Extract Constant Selection.compile_switch => "Switchaux.compile_switch". +Extract Constant Selection.if_conversion_heuristic => "Selectionaux.if_conversion_heuristic". (* RTLgen *) Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely". @@ -166,11 +167,11 @@ Load extractionMachdep. Extraction Blacklist List String Int. (* 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". -Extract Inlined Constant Fappli_IEEE.round_mode => "fun _ -> assert false". -Extract Inlined Constant Fcalc_bracket.inbetween_loc => "fun _ -> assert false". +Extract Inlined Constant Defs.F2R => "fun _ -> assert false". +Extract Inlined Constant Binary.FF2R => "fun _ -> assert false". +Extract Inlined Constant Binary.B2R => "fun _ -> assert false". +Extract Inlined Constant Binary.round_mode => "fun _ -> assert false". +Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. |