Changeset 1411 for src/LIN


Ignore:
Timestamp:
Oct 19, 2011, 1:39:54 PM (8 years ago)
Author:
sacerdot
Message:
  1. sem_params2 splitted into sem_params1 + sem_params2 to take out the semantics of the extended statements
  2. pointer call semantics given in RTL/semantics
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1408 r1411  
    5555 ∀globals. more_sem_params2 … (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) ≝
    5656 λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
    57   mk_more_sem_params2 … (ltl_lin_more_sem_params … succ pointer_of_label)
    58    (fetch globals) (load_ra …) (ltl_lin_result_regs …)
    59    ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …)
    60    (ltl_lin_fetch_external_args …) (ltl_lin_set_result …) (ltl_lin_exec_extended …).
     57  mk_more_sem_params2 …
     58   (mk_more_sem_params1 … (ltl_lin_more_sem_params … succ pointer_of_label)
     59    (fetch globals) (load_ra …) (ltl_lin_result_regs …)
     60    ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …)
     61    (ltl_lin_fetch_external_args …) (ltl_lin_set_result …)) (ltl_lin_exec_extended …).
    6162
    6263definition ltl_lin_fullexec ≝
Note: See TracChangeset for help on using the changeset viewer.