From 94fc497484b675fd2bc57d6c477416f771730223 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 11 Sep 2006 12:39:06 +0000 Subject: 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(-) (limited to 'extraction') diff --git a/extraction/Kildall.ml.patch b/extraction/Kildall.ml.patch index a091385..a5b7bc9 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 **) + -- cgit v1.2.3