Changeset 1283 for src/RTLabs
 Timestamp:
 Sep 30, 2011, 3:12:40 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1282 r1283 158 158 definition translate_move_internal ≝ 159 159 λglobals. 160 λstart_lbl: label.161 160 λdestr: register. 162 161 λsrcr: register. 163 sequential rtl_params_ globals (MOVE … 〈destr,srcr〉) start_lbl.162 sequential rtl_params_ globals (MOVE … 〈destr,srcr〉). 164 163 165 164 definition translate_move ≝ … … 174 173 let restl ≝ \snd (\fst crl_crr) in 175 174 let restr ≝ \snd (\snd crl_crr) in 176 let f_common ≝ translate_move_internal globals start_lblin175 let f_common ≝ translate_move_internal globals in 177 176 let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in 178 177 let translate2 ≝ translate_cst … (Ointconst ? (repr I8 0)) restl in (* should this be 8? *) … … 212 211 add_translates … [ 213 212 adds_graph rtl_params1 … [ 214 sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) start_lbl213 sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) 215 214 ]; 216 215 translate_move globals destrs zeros
Note: See TracChangeset
for help on using the changeset viewer.