Changeset 2182 for src/ERTL/liveness_paolo.ma
- Timestamp:
- Jul 13, 2012, 11:20:36 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/liveness_paolo.ma
r2174 r2182 3 3 include "utilities/adt/set_adt.ma". 4 4 include "utilities/fixpoints.ma". 5 6 (* maybe move? *)7 definition stmt_successors :8 ∀p : graph_params.∀globals.joint_statement p globals → list label ≝9 λp,g,s.match s with10 [ sequential seq l ⇒11 (match seq with12 [ COND _ lbl_true ⇒ [ lbl_true ]13 | _ ⇒ [ ]14 ]) @ [ l ]15 | final fin ⇒16 match fin with17 [ GOTO l ⇒ [ l ]18 | _ ⇒ [ ]19 ]20 ].21 5 22 6 definition register_lattice : property_lattice ≝ … … 268 252 [ None ⇒ rl_bottom 269 253 | Some stmt ⇒ 270 \fold[rl_join,rl_bottom]_{successor ∈ stmt_ successors … stmt}254 \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt} 271 255 (livebefore globals int_fun successor liveafter) 272 256 ].
Note: See TracChangeset
for help on using the changeset viewer.