Changeset 1165


Ignore:
Timestamp:
Sep 1, 2011, 5:18:33 PM (8 years ago)
Author:
mulligan
Message:

more changes

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1163 r1165  
    1414
    1515definition pre_ertl_statement ≝
    16   λglobals: list ident.
    17   joint_statement label globals register
    18                   register register register
     16  joint_statement label register register register register
    1917                  (move_registers × move_registers) register.
    2018                 
  • src/ERTL/ERTLToLTL.ma

    r1163 r1165  
    5151    sub.
    5252
    53 check
    54 
    5553definition get_stack ≝
    56   λglobals.
     54  λglobals: list ident.
    5755  λint_fun.
    5856  λgraph: graph (ltl_statement (globals)).
     
    6260    let off ≝ adjust_off globals int_fun off in
    6361    let luniv ≝ ertl_if_luniverse globals int_fun in
    64     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_hdw_to_hdw globals … 〈RegisterA, r〉) l) in
     62    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential  globals (joint_instr_move … globals (from_acc r)) l) in
    6563    ?.
    6664   
Note: See TracChangeset for help on using the changeset viewer.