Changeset 1384 for src/LIN


Ignore:
Timestamp:
Oct 16, 2011, 7:42:25 PM (8 years ago)
Author:
sacerdot
Message:
  • fetch_ra taken out of pop_frame again since it is used uniformly and it is also required for is_final
  • fetch_ra made abstract since it gets a different implementation in RTL
  • old fetch_ra renamed into load_ra (to match the save_ra name)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1383 r1384  
    2828definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    2929definition ltl_lin_pop_frame:
    30  ∀succT,succ,pointer_of_label. state … (ltl_lin_sem_params succT succ pointer_of_label) → res ((state … (ltl_lin_sem_params … succ pointer_of_label)) × address) ≝
    31  λ_.λ_.λ_.fetch_ra ….
     30 ∀succT,succ,pointer_of_label. state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝
     31 λ_.λ_.λ_.λt.OK … t.
    3232definition ltl_lin_save_frame:
    3333 ∀succT,succ,pointer_of_label. address → nat → unit → nat → unit → state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝
     
    5555 λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
    5656  mk_more_sem_params2 … (ltl_lin_more_sem_params1 … succ pointer_of_label)
    57    (fetch globals) (ltl_lin_fetch_result …) (ltl_lin_fetch_external_args …)
     57   (fetch globals) (load_ra …) (ltl_lin_fetch_result …)
     58   (ltl_lin_fetch_external_args …)
    5859   (ltl_lin_set_result …) (ltl_lin_exec_extended …).
    5960
Note: See TracChangeset for help on using the changeset viewer.