Changeset 2942 for src/ERTL


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/ERTL/ERTLtoERTLptrOK.ma

    r2940 r2942  
    862862         (inr ident … 〈c_ptr1,c_ptr2〉)
    863863         (sigma_state_pc prog f_lbls f_regs st2))
    864         [
    865        
    866        generalize in match (block_of_call ?????);
    867        
    868        %
     864         
     865         [ whd in ⊢ (??%%); normalize nodelta
     866         XXX
     867         %
    869868  |*:  whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
    870869      @if_elim change with (pc_block(pc … st2)) in match (pc_block ?);
Note: See TracChangeset for help on using the changeset viewer.