From 94fc497484b675fd2bc57d6c477416f771730223 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 11 Sep 2006 12:39:06 +0000
Subject: [PATCH] Encore une eta-expansion intempestive
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@90 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
extraction/Kildall.ml.patch | 27 +++++++++++++++++++++++----
1 file changed, 23 insertions(+), 4 deletions(-)
diff --git a/extraction/Kildall.ml.patch b/extraction/Kildall.ml.patch
index a091385d9..a5b7bc93b 100644
--- a/extraction/Kildall.ml.patch
+++ b/extraction/Kildall.ml.patch
@@ -1,7 +1,7 @@
-*** Kildall.ml.orig 2006-02-09 11:47:52.000000000 +0100
---- Kildall.ml 2006-02-09 13:42:35.103321691 +0100
+*** Kildall.ml.orig 2006-09-11 13:50:56.266682206 +0200
+--- Kildall.ml 2006-09-11 14:29:50.392200227 +0200
***************
-*** 191,199 ****
+*** 163,171 ****
Maps.PMap.t option **)
let fixpoint successors topnode transf entrypoints =
@@ -11,7 +11,7 @@
end
module type ORDERED_TYPE_WITH_TOP =
---- 191,198 ----
+--- 163,170 ----
Maps.PMap.t option **)
let fixpoint successors topnode transf entrypoints =
@@ -20,3 +20,22 @@
end
module type ORDERED_TYPE_WITH_TOP =
+***************
+*** 264,271 ****
+ (** val basic_block_map : (positive -> positive list) -> positive ->
+ positive -> bbmap **)
+
+! let basic_block_map successors topnode entrypoint x =
+! is_basic_block_head entrypoint (make_predecessors successors topnode) x
+
+ (** val basic_block_list : positive -> bbmap -> positive list **)
+
+--- 263,270 ----
+ (** val basic_block_map : (positive -> positive list) -> positive ->
+ positive -> bbmap **)
+
+! let basic_block_map successors topnode entrypoint =
+! is_basic_block_head entrypoint (make_predecessors successors topnode)
+
+ (** val basic_block_list : positive -> bbmap -> positive list **)
+
--
GitLab