diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-16 15:35:09 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-16 15:35:09 +0000 |
| commit | 4b119d6f9f0e846edccaf5c08788ca1615b22526 (patch) | |
| tree | 66cf55decd8d950d0bdc1050448aa3ee448ca13a /extraction | |
| parent | 1fe28ba1ec3dd0657b121c4a911ee1cb046bab09 (diff) | |
Cil2Csyntax: added goto and labels; added assignment between structs
Kildall: simplified the interface
Constprop, CSE, Allocation, Linearize: updated for the new Kildall
RTL, LTL: removed the well-formedness condition on the CFG,
it is no longer necessary with the new Kildall and it is problematic
for validated optimizations.
Maps: more efficient implementation of PTree.fold.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1124 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/Kildall.ml.patch | 47 |
1 files changed, 14 insertions, 33 deletions
diff --git a/extraction/Kildall.ml.patch b/extraction/Kildall.ml.patch index b7e5b0b..6c94854 100644 --- a/extraction/Kildall.ml.patch +++ b/extraction/Kildall.ml.patch @@ -1,40 +1,21 @@ -*** kildall.ml.orig 2009-06-03 11:32:52.297641897 +0200 ---- kildall.ml 2009-06-03 11:34:48.481516509 +0200 +*** kildall.ml.orig 2009-08-16 15:45:21.000000000 +0200 +--- kildall.ml 2009-08-16 15:45:27.000000000 +0200 *************** -*** 151,158 **** - -> (positive, LAT.t) prod list -> LAT.t PMap.t option **) +*** 252,259 **** - let fixpoint successors topnode transf entrypoints = -! DS.fixpoint (fun s -> PMap.get s (make_predecessors successors topnode)) -! topnode transf entrypoints - end - - module type ORDERED_TYPE_WITH_TOP = ---- 151,158 ---- - -> (positive, LAT.t) prod list -> LAT.t PMap.t option **) + (** val basic_block_map : positive list PTree.t -> positive -> bbmap **) - let fixpoint successors topnode transf entrypoints = -! let pred = make_predecessors successors topnode in -! DS.fixpoint (fun s -> PMap.get s pred) topnode transf entrypoints - end - - module type ORDERED_TYPE_WITH_TOP = -*************** -*** 248,255 **** - (** 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 **) +! let basic_block_map successors entrypoint x = +! is_basic_block_head entrypoint (make_predecessors successors) x ---- 248,255 ---- - (** val basic_block_map : - (positive -> positive list) -> positive -> positive -> bbmap **) + (** val basic_block_list : + positive list PTree.t -> bbmap -> positive list **) +--- 252,259 ---- -! let basic_block_map successors topnode entrypoint = -! is_basic_block_head entrypoint (make_predecessors successors topnode) + (** val basic_block_map : positive list PTree.t -> positive -> bbmap **) - (** val basic_block_list : positive -> bbmap -> positive list **) +! let basic_block_map successors entrypoint = +! is_basic_block_head entrypoint (make_predecessors successors) + (** val basic_block_list : + positive list PTree.t -> bbmap -> positive list **) |