diff --git a/extraction/Kildall.ml.patch b/extraction/Kildall.ml.patch index a091385d9a8e07a15dc86226057d016239918894..a5b7bc93b636c04ec5347b46d7b4ce83e13b4588 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 **) +