Changeset 1324 for src/LIN


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/LIN/semantics.ma

    r1312 r1324  
    4343axiom lin_set_result: list val → state lin_sem_params → res (state lin_sem_params).
    4444
    45 definition lin_exec_extended: ∀globals. genv globals (lin_params globals) → False → state lin_sem_params → IO io_out io_in (trace × (state lin_sem_params))
     45definition lin_exec_extended: ∀globals. genv globals (lin_params globals) → False → unit → state lin_sem_params → IO io_out io_in (trace × (state lin_sem_params))
    4646 ≝ λglobals,ge,abs. ⊥.
    4747@abs qed.
Note: See TracChangeset for help on using the changeset viewer.