Ignore:
Timestamp:
Oct 7, 2011, 3:32:07 PM (8 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1312 r1324  
    8181 ; set_result: list val → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1))
    8282
    83  ; 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)))
     83 ; 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)))
    8484 }.
    8585
     
    220220    | sequential seq l ⇒
    221221      match seq with
    222       [ extension c ⇒ exec_extended … p ge c st
     222      [ extension c ⇒ exec_extended … p ge c l st
    223223      | COST_LABEL cl ⇒ ret ? 〈Echarge cl, next … l st〉
    224224      | COMMENT c ⇒ ret ? 〈E0, next … l st〉
Note: See TracChangeset for help on using the changeset viewer.