Changeset 2566


Ignore:
Timestamp:
Dec 19, 2012, 6:55:08 PM (7 years ago)
Author:
piccolo
Message:

ERTL to ERTLptr pass implemented up to a few things to be
left to the infrastructure (marked with PAOLO)

Location:
src
Files:
4 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r2564 r2566  
    119119axiom FunctionNotFound: errmsg.
    120120
     121(*CSC: here we should use helper_def_store from Joint/semantics.ma,
     122  but it is not visible *)
     123definition ps_reg_store_status : register → beval → state ERTL_state →
     124  res (state ERTL_state) ≝
     125 λdst,v,st.
     126  let env ≝ regs … st in
     127  ! env' ← ps_reg_store dst v env ;
     128  let env'' ≝ 〈add_need_spilled_no dst (\fst env'), \snd env'〉 in
     129  return set_regs ERTL_state env'' st.
     130
    121131definition eval_ertl_seq:
    122132 ∀F. ∀globals. genv_gen F globals →
     
    135145      let newsp ≝ shift_pointer … sp framesize in
    136146      return set_hwsp newsp st
    137    | ertl_frame_size dst ⇒
    138       let env ≝ regs … st in
    139       ! env' ← ps_reg_store dst (BVByte framesize) env ;
    140       let env'' ≝ 〈add_need_spilled_no dst (\fst env'), \snd env'〉 in
    141       return set_regs ERTL_state env'' st
     147   | ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st
    142148   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed. 
    143149
Note: See TracChangeset for help on using the changeset viewer.