Changeset 1384 for src/LIN

Timestamp:

Oct 16, 2011, 7:42:25 PM (10 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:

• src/LIN/joint_LTL_LIN_semantics.ma (modified) (2 diffs)

src/LIN/joint_LTL_LIN_semantics.ma

@@ -28 +28 @@
 definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
 definition ltl_lin_pop_frame:
- ∀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) ≝
- λ_.λ_.λ_.fetch_ra ….
+ ∀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)) ≝
+ λ_.λ_.λ_.λt.OK … t.
 definition ltl_lin_save_frame:
  ∀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)) ≝
@@ -55 +55 @@
  λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
   mk_more_sem_params2 … (ltl_lin_more_sem_params1 … succ pointer_of_label)
-   (fetch globals) (ltl_lin_fetch_result …) (ltl_lin_fetch_external_args …)
+   (fetch globals) (load_ra …) (ltl_lin_fetch_result …)
+   (ltl_lin_fetch_external_args …)
    (ltl_lin_set_result …) (ltl_lin_exec_extended …).