Ignore:
Timestamp:
Oct 6, 2011, 12:16:22 AM (8 years ago)
Author:
sacerdot
Message:
  1. LTL/semantics.ma added (work in progress)
  2. init_locals fixed to take in input the old register environment, since physical registers should just be left untouched
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1298 r1303  
    5858 { more_sparams:> more_sem_params p
    5959
    60  ; init_locals : localsT p → regsT … more_sparams
     60 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
    6161 
    6262 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
     
    289289            ! st ← save_ra … st l;
    290290              let st ≝ save_frame … st in
    291               let regs ≝ init_locals … (joint_if_locals … fn) in
     291              let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    292292              let l' ≝ joint_if_entry … fn in
    293293             ret ? 〈 E0, goto … l' (set_regs p regs st)〉
Note: See TracChangeset for help on using the changeset viewer.