Changeset 1283 for src/RTLabs


Ignore:
Timestamp:
Sep 30, 2011, 3:12:40 AM (8 years ago)
Author:
sacerdot
Message:

Bad programming practice removed: change_label is no longer required and
add_graph now takes function from label to statements in place of taking
statements containing a wrong label to be fixed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1282 r1283  
    158158definition translate_move_internal ≝
    159159  λglobals.
    160   λstart_lbl: label.
    161160  λdestr: register.
    162161  λsrcr: register.
    163     sequential rtl_params_ globals (MOVE … 〈destr,srcr〉) start_lbl.
     162    sequential rtl_params_ globals (MOVE … 〈destr,srcr〉).
    164163
    165164definition translate_move ≝
     
    174173      let restl ≝ \snd (\fst crl_crr) in
    175174      let restr ≝ \snd (\snd crl_crr) in
    176       let f_common ≝ translate_move_internal globals start_lbl in
     175      let f_common ≝ translate_move_internal globals in
    177176      let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in
    178177      let translate2 ≝ translate_cst … (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
     
    212211    add_translates … [
    213212      adds_graph rtl_params1 … [
    214         sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) start_lbl
     213        sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0))
    215214        ];
    216215      translate_move globals destrs zeros
Note: See TracChangeset for help on using the changeset viewer.