Changeset 1372 for src/LIN/semantics.ma


Ignore:
Timestamp:
Oct 14, 2011, 2:48:34 PM (8 years ago)
Author:
sacerdot
Message:

save_frame now takes the stacksize to allow RTL to allocate the stack frame

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/semantics.ma

    r1371 r1372  
    2727definition lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    2828definition lin_pop_frame: list beval → state … lin_sem_params → res (state … lin_sem_params) ≝ λ_.λst. OK … st.
    29 definition lin_save_frame: unit → nat → unit → state … lin_sem_params → res (state … lin_sem_params) ≝ λ_.λ_.λ_.λst.OK … st.
     29definition lin_save_frame: nat → unit → nat → unit → state … lin_sem_params → res (state … lin_sem_params) ≝ λ_.λ_.λ_.λ_.λst.OK … st.
    3030
    3131definition lin_more_sem_params1 : more_sem_params1 … lin_params1 ≝
Note: See TracChangeset for help on using the changeset viewer.