Changeset 1411 for src/ERTL


Ignore:
Timestamp:
Oct 19, 2011, 1:39:54 PM (9 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/ERTL/semantics.ma

    r1408 r1411  
    117117definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
    118118 λglobals.
    119   mk_more_sem_params2 … ertl_more_sem_params
    120    (graph_fetch_statement …) (load_ra …) (ertl_result_regs …)
    121    ertl_init_locals ertl_save_frame (ertl_pop_frame …)
    122    ertl_fetch_external_args ertl_set_result (ertl_exec_extended …).
     119  mk_more_sem_params2 …
     120   (mk_more_sem_params1 … ertl_more_sem_params
     121    (graph_fetch_statement …) (load_ra …) (ertl_result_regs …)
     122    ertl_init_locals ertl_save_frame (ertl_pop_frame …)
     123    ertl_fetch_external_args ertl_set_result)
     124   (ertl_exec_extended …).
    123125
    124126definition ertl_fullexec ≝
Note: See TracChangeset for help on using the changeset viewer.