Changeset 1282 for src/RTLabs/RTLAbstoRTL.ma
 Timestamp:
 Sep 28, 2011, 11:50:32 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1281 r1282 144 144 145 145 definition translate_cst_int_internal ≝ 146 λglobals,dest_lbl,r,i. joint_st_sequential rtl_params_ globals (joint_instr_int… r i) dest_lbl.146 λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl. 147 147 148 148 (*CSC: XXXXX *) … … 161 161 λdestr: register. 162 162 λsrcr: register. 163 joint_st_sequential rtl_params_ globals (joint_instr_move… 〈destr,srcr〉) start_lbl.163 sequential rtl_params_ globals (MOVE … 〈destr,srcr〉) start_lbl. 164 164 165 165 definition translate_move ≝ … … 212 212 add_translates … [ 213 213 adds_graph rtl_params1 … [ 214 joint_st_sequential rtl_params_ … (joint_instr_intrtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) start_lbl214 sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) start_lbl 215 215 ]; 216 216 translate_move globals destrs zeros … … 1015 1015 λdef: joint_internal_function … (rtl_params globals). 1016 1016 match stmt with 1017 [ St_skip lbl' ⇒ add_graph … lbl ( joint_st_goto… lbl') def1017 [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def 1018 1018  _ ⇒ ? ]. 1019 1019 (* … … 1087 1087 let entry' ≝ f_entry def in 1088 1088 let exit' ≝ f_exit def in 1089 let graph' ≝ add … (empty_map ? ?) entry' ( joint_st_goto… entry') in1090 let graph' ≝ add … graph' exit' ( joint_st_goto… exit') in1089 let graph' ≝ add … (empty_map ? ?) entry' (GOTO … entry') in 1090 let graph' ≝ add … graph' exit' (GOTO … exit') in 1091 1091 let res ≝ 1092 1092 mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params'
Note: See TracChangeset
for help on using the changeset viewer.