Changeset 1384 for src/RTL/semantics.ma


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/RTL/semantics.ma

    r1381 r1384  
    3232axiom OutOfBounds: String.
    3333
     34definition rtl_fetch_ra:
     35 state … rtl_sem_params → res ((state … rtl_sem_params) × address) ≝
     36 λst.
     37  match st_frms ? st with
     38  [ nil ⇒ Error ? [MSG EmptyStack]
     39  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
     40
     41
    3442(*CSC: XXXXX, for is_final only *)
    3543axiom rtl_fetch_result: state rtl_sem_params → res (list beval).
     
    4149  saves the OutOfBounds exception *)
    4250definition rtl_pop_frame:
    43  state … rtl_sem_params → res ((state … rtl_sem_params) × address) ≝
     51 state … rtl_sem_params → res (state … rtl_sem_params) ≝
    4452 λst.
    4553  do ret_vals ← rtl_fetch_result … st ;
     
    5563       (OK … st) (fr_ret_regs hd) ;
    5664     OK …
    57       set_frms rtl_sem_params tl
     65      (set_frms rtl_sem_params tl
    5866        (set_regs rtl_sem_params (fr_regs hd)
    5967         (set_sp … (fr_sp hd)
    6068          (set_carry … (fr_carry hd)
    61            (set_m … (free … (m … st) (pblock (sp … st))) st)))),
    62        fr_pc hd〉 ].
     69           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
    6370
    6471definition rtl_save_frame:
     
    111118 λglobals.
    112119  mk_more_sem_params2 … rtl_more_sem_params1
    113    (graph_fetch_statement …) rtl_fetch_result rtl_fetch_external_args rtl_set_result
    114     (rtl_exec_extended …).
     120   (graph_fetch_statement …) rtl_fetch_ra rtl_fetch_result rtl_fetch_external_args
     121    rtl_set_result (rtl_exec_extended …).
    115122
    116123definition rtl_fullexec ≝
Note: See TracChangeset for help on using the changeset viewer.