Changeset 1324 for src/ERTL/semantics.ma


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1318 r1324  
    6565axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params).
    6666
    67 axiom ertl_exec_extended: ∀globals. genv globals (ertl_params globals) → ertl_statement_extension → state ertl_sem_params → IO io_out io_in (trace × (state ertl_sem_params)).
     67axiom ertl_exec_extended: ∀globals. genv globals (ertl_params globals) → ertl_statement_extension → label → state ertl_sem_params → IO io_out io_in (trace × (state ertl_sem_params)).
    6868
    6969definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
Note: See TracChangeset for help on using the changeset viewer.