Changeset 1150


Ignore:
Timestamp:
Aug 30, 2011, 4:23:37 PM (8 years ago)
Author:
sacerdot
Message:

Push/pop implemented.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1148 r1150  
    318318      let pc ≝ address_of_address_chunks pcl pch in
    319319      ret ? 〈E0,set_pc pc st〉
    320   | _ ⇒ ? ].
     320 
     321  (* CSC: new stuff *)
     322  | ertl_st_comment _ l ⇒ ret ? 〈E0, goto l st〉
     323  | ertl_st_new_frame _ ⇒ ?
     324  | ertl_st_del_frame _ ⇒ ?
     325  | ertl_st_frame_size _ _ ⇒ ?
     326  | ertl_st_pop dst l ⇒
     327     ! 〈st,v〉 ← pop st;
     328     ! locals ← reg_store dst (val_of_Byte v) (locals st);
     329     ret ? 〈E0, goto l (set_locals locals st)〉
     330  | ertl_st_push src l ⇒
     331     ! v ← reg_retrieve (locals st) src;
     332     ! v ← Byte_of_val v;
     333     ! st ← push st v;
     334     ret ? 〈E0, goto l st〉
     335  ].
    321336
    322337axiom WrongReturnValueType: String.
Note: See TracChangeset for help on using the changeset viewer.