Changeset 2182 for src/ERTL/liveness_paolo.ma

Timestamp:

Jul 13, 2012, 11:20:36 AM (8 years ago)

Author:

tranquil

Message:

updated linearisation pass

File:

• src/ERTL/liveness_paolo.ma (modified) (2 diffs)

src/ERTL/liveness_paolo.ma

@@ -3 +3 @@
 include "utilities/adt/set_adt.ma".
 include "utilities/fixpoints.ma".
-
-(* maybe move? *)
-definition stmt_successors :
-  ∀p : graph_params.∀globals.joint_statement p globals → list label ≝
-  λp,g,s.match s with
-  [ sequential seq l ⇒
-    (match seq with
-     [ COND _ lbl_true ⇒ [ lbl_true ]
-     | _ ⇒ [ ]
-     ]) @ [ l ]
-  | final fin ⇒ 
-    match fin with
-    [ GOTO l ⇒ [ l ]
-    | _ ⇒ [ ]
-    ]
-  ].
 
 definition register_lattice : property_lattice ≝
@@ -268 +252 @@
   [ None      ⇒ rl_bottom
   | Some stmt ⇒
-    \fold[rl_join,rl_bottom]_{successor ∈ stmt_successors … stmt}
+    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
       (livebefore globals int_fun successor liveafter)
   ].