Changeset 1303 for src/joint

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:

• src/joint/semantics.ma (modified) (2 diffs)

src/joint/semantics.ma

@@ -58 +58 @@
  { more_sparams:> more_sem_params p
 
- ; init_locals : localsT p → regsT … more_sparams
+ ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
  
  ; 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;
               let st ≝ save_frame … st in
-              let regs ≝ init_locals … (joint_if_locals … fn) in
+              let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
               let l' ≝ joint_if_entry … fn in
              ret ? 〈 E0, goto … l' (set_regs p regs st)〉