Changeset 2942 for src/ERTLptr/liveness.ma

Timestamp:

Mar 23, 2013, 1:37:22 AM (8 years ago)

Author:

sacerdot

Message:

Many changes:

1. Coloured graphs are now specified in terms of livebefore
2. Type of livebefore changed so that it is now a valuation transformer
3. Several axioms can now be inhabited in ERTLptrToLTLProof

Problems:
ERTLtoERTLptrOK is broken beyond my understanding. This pass should have
been unaffected by the changes, but it is not so. Why?

File:

• src/ERTLptr/liveness.ma (modified) (2 diffs)

src/ERTLptr/liveness.ma

@@ -232 +232 @@
     rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt).
 
-definition livebefore ≝
+definition livebefore:
+  ∀globals: list ident.
+   joint_internal_function ERTLptr globals →
+     valuation register_lattice → valuation register_lattice
+≝
   λglobals: list ident.
   λint_fun: joint_internal_function ERTLptr globals.
+  λliveafter: valuation register_lattice.
   λlabel.
-  λliveafter: valuation register_lattice.
   match lookup ?? (joint_if_code … int_fun) label with
   [ None      ⇒ rl_bottom
@@ -251 +255 @@
   | Some stmt ⇒
     \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
-      (livebefore globals int_fun successor liveafter)
+      (livebefore globals int_fun liveafter successor)
   ].