Changeset 1388 for src/ERTL/semantics.ma


Ignore:
Timestamp:
Oct 17, 2011, 10:54:50 AM (9 years ago)
Author:
sacerdot
Message:

fetch_result implemented for ERTL. This required a different istantiation of
resultT that is not in line with the OCaml's code. Look at CHANGES for details.
RTLToERTL has been ported in an hopefully correct manner.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1386 r1388  
    6060    (set_regs ertl_sem_params 〈empty_map …,\snd (regs … st)〉 st)).
    6161
    62 (*CSC: XXXXX, for is_final only *)
    63 axiom ertl_fetch_result:
    64  ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list beval).
     62definition ertl_fetch_result:
     63 ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list beval) ≝
     64 λglobals,ge,st.
     65  do fn ← graph_fetch_function … globals ge st ;
     66  let ret_val_regs ≝ joint_if_result … fn in
     67   mmap … (λreg.greg_retrieve ertl_sem_params st reg) ret_val_regs.
    6568
    6669(*CSC: XXXX, for external functions only*)
Note: See TracChangeset for help on using the changeset viewer.