Changeset 1377 for src/LTL


Ignore:
Timestamp:
Oct 14, 2011, 7:22:59 PM (8 years ago)
Author:
sacerdot
Message:

pop_frame now incorporates the fetch_result (that made sense only for RTL).
pop_frame and save_frame are now also more symmetric

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/semantics.ma

    r1372 r1377  
    2121
    2222definition ltl_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    23 definition ltl_pop_frame: list beval → state … ltl_sem_params → res (state … ltl_sem_params) ≝ λ_.λst. OK … st.
    24 definition ltl_save_frame: nat → unit → nat → unit → state … ltl_sem_params → res (state … ltl_sem_params) ≝ λ_.λ_.λ_.λ_.λst.OK … st.
     23definition ltl_pop_frame: state … ltl_sem_params → res ((state … ltl_sem_params) × address) ≝
     24 fetch_ra ….
     25definition ltl_save_frame:
     26 address → nat → unit → nat → unit → state … ltl_sem_params → res (state … ltl_sem_params) ≝
     27 λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
    2528
    2629definition ltl_more_sem_params1 : more_sem_params1 … ltl_params1 ≝
Note: See TracChangeset for help on using the changeset viewer.