Changeset 1390 for src/RTL


Ignore:
Timestamp:
Oct 17, 2011, 11:43:52 AM (9 years ago)
Author:
sacerdot
Message:

All fetch_result implementations have been factorized out, leaving only a
result_regs function. All axioms in joint_LTL_LIN_semantics but the ones for
external functions have been implemented.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1386 r1390  
    3939  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
    4040
    41 definition rtl_fetch_result:
    42  ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (list beval) ≝
     41definition rtl_result_regs:
     42 ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (list register) ≝
    4343 λglobals,ge,st.
    4444  do fn ← graph_fetch_function … globals ge st ;
    45   let ret_val_regs ≝ joint_if_result … fn in
    46    mmap … (λreg.greg_retrieve rtl_sem_params st reg) ret_val_regs.
     45  OK … (joint_if_result … fn).
    4746
    4847(*CSC: we could use a dependent type here: the list of return values should have
     
    5251 ∀globals. genv … (rtl_params globals) → state … rtl_sem_params → res (state … rtl_sem_params) ≝
    5352 λglobals,ge,st.
    54   do ret_vals ← rtl_fetch_result … ge st ;
     53  do ret_regs ← rtl_result_regs … ge st ;
     54  do ret_vals ← mmap … (λreg.greg_retrieve rtl_sem_params st reg) ret_regs ;
    5555  match st_frms ? st with
    5656  [ nil ⇒ Error ? [MSG EmptyStack]
     
    114114 λglobals.
    115115  mk_more_sem_params2 … rtl_more_sem_params
    116    (graph_fetch_statement …) rtl_fetch_ra (rtl_fetch_result …)
     116   (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
    117117   rtl_init_locals rtl_save_frame (rtl_pop_frame …)
    118118   rtl_fetch_external_args rtl_set_result (rtl_exec_extended …).
Note: See TracChangeset for help on using the changeset viewer.