- Timestamp:
- Oct 6, 2011, 12:16:22 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/semantics.ma
r1298 r1303 58 58 { more_sparams:> more_sem_params p 59 59 60 ; init_locals : localsT p → regsT … more_sparams 60 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams 61 61 62 62 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals) … … 289 289 ! st ← save_ra … st l; 290 290 let st ≝ save_frame … st in 291 let regs ≝ init_locals … (joint_if_locals … fn) in291 let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in 292 292 let l' ≝ joint_if_entry … fn in 293 293 ret ? 〈 E0, goto … l' (set_regs p regs st)〉
Note: See TracChangeset
for help on using the changeset viewer.