Changeset 1282 for src/RTLabs


Ignore:
Timestamp:
Sep 28, 2011, 11:50:32 PM (8 years ago)
Author:
sacerdot
Message:

Cosmetic change: names of joint statements/instructions shortened and made
uppercase.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1281 r1282  
    144144
    145145definition 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.
    147147
    148148(*CSC: XXXXX *)
     
    161161  λdestr: register.
    162162  λ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.
    164164
    165165definition translate_move ≝
     
    212212    add_translates … [
    213213      adds_graph rtl_params1 … [
    214         joint_st_sequential rtl_params_ … (joint_instr_int rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) start_lbl
     214        sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) start_lbl
    215215        ];
    216216      translate_move globals destrs zeros
     
    10151015  λdef: joint_internal_function … (rtl_params globals).
    10161016  match stmt with
    1017   [ St_skip lbl' ⇒ add_graph … lbl (joint_st_goto … lbl') def
     1017  [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def
    10181018  | _ ⇒ ? ].
    10191019(*
     
    10871087  let entry' ≝ f_entry def in
    10881088  let exit' ≝ f_exit def in
    1089   let graph' ≝ add … (empty_map ? ?) entry' (joint_st_goto … entry') in
    1090   let graph' ≝ add … graph' exit' (joint_st_goto … exit') in
     1089  let graph' ≝ add … (empty_map ? ?) entry' (GOTO … entry') in
     1090  let graph' ≝ add … graph' exit' (GOTO … exit') in
    10911091  let res ≝
    10921092    mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params'
Note: See TracChangeset for help on using the changeset viewer.