Changeset 1275 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Sep 26, 2011, 6:07:47 PM (8 years ago)
Author:
sacerdot
Message:

RTL ported to joint syntax, but:

  1. bug discovered: opaccs should have taken four registers
  2. push/pop should not be present in RTL :-(

ERTLToLTL and RTLtoERTL not working ATM

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1274 r1275  
    22include "LTL/LTL.ma".
    33include "ERTL/spill.ma".
    4 include "ERTL/uses.ma".
    54include "ASM/Arithmetic.ma".
    65
     
    396395          〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_int … hdw (bitvector_of_nat … (stacksize … int_fun))) l) graph, luniv〉
    397396      ]
    398     | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
     397    | joint_instr_opaccs opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    399398      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    400399      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
Note: See TracChangeset for help on using the changeset viewer.