Changeset 1324 for src/joint

Timestamp:

Oct 7, 2011, 3:32:07 PM (9 years ago)

Author:

sacerdot

Message:

The semantics of extended statements must also consider the label since
the program counter is not automatically incremented
(because of cond instructions :-(

File:

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

src/joint/semantics.ma

@@ -81 +81 @@
  ; set_result: list val → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1))
 
- ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams1) → state (mk_sem_params … more_sparams1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams1)))
+ ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams1) → succ p → state (mk_sem_params … more_sparams1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams1)))
  }.
 
@@ -220 +220 @@
     | sequential seq l ⇒
       match seq with
-      [ extension c ⇒ exec_extended … p ge c st
+      [ extension c ⇒ exec_extended … p ge c l st
       | COST_LABEL cl ⇒ ret ? 〈Echarge cl, next … l st〉
       | COMMENT c ⇒ ret ? 〈E0, next … l st〉