diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-11 12:39:06 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-11 12:39:06 +0000 |
| commit | 94fc497484b675fd2bc57d6c477416f771730223 (patch) | |
| tree | 2bde2c3806019107eafa0bbfba0d32ae66c034a7 /extraction | |
| parent | 71f3ecc437f3147e7cf3490f14a78901cb344dc8 (diff) | |
Encore une eta-expansion intempestive
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@90 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/Kildall.ml.patch | 27 |
1 files changed, 23 insertions, 4 deletions
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 **) + |