Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/liveness.ma

    r2887 r2942  
    232232    rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt).
    233233
    234 definition livebefore ≝
     234definition livebefore:
     235  ∀globals: list ident.
     236   joint_internal_function ERTLptr globals →
     237     valuation register_lattice → valuation register_lattice
     238
    235239  λglobals: list ident.
    236240  λint_fun: joint_internal_function ERTLptr globals.
     241  λliveafter: valuation register_lattice.
    237242  λlabel.
    238   λliveafter: valuation register_lattice.
    239243  match lookup ?? (joint_if_code … int_fun) label with
    240244  [ None      ⇒ rl_bottom
     
    251255  | Some stmt ⇒
    252256    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
    253       (livebefore globals int_fun successor liveafter)
     257      (livebefore globals int_fun liveafter successor)
    254258  ].
    255259
Note: See TracChangeset for help on using the changeset viewer.