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

    r1387 r1390  
    5656
    5757 ; fetch_ra: state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)) × address)
    58  ; fetch_result: genv globals p → state (mk_sem_params … more_sparams1) → res (list beval)
     58 ; result_regs: genv globals p → state (mk_sem_params … more_sparams1) → res (list (generic_reg p))
    5959
    6060 ; init_locals : localsT p → regsT … more_sparams1 → regsT … more_sparams1
     
    328328      do 〈st,ra〉 ← fetch_ra … st;
    329329      if eq_address ra exit then
    330        do vals ← fetch_result … ge st ;
     330       do regs ← result_regs … ge st ;
     331       do vals ← mmap … (λreg.greg_retrieve … st reg) regs ;
    331332       Word_of_list_beval vals
    332333      else
Note: See TracChangeset for help on using the changeset viewer.