Ignore:
Timestamp:
Mar 18, 2011, 12:11:23 PM (10 years ago)
Author:
campbell
Message:

Separate out whole program executions from the clight semantics and start
setting it up for RTLabs too.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Animation.ma

    r487 r693  
    1313].
    1414
    15 let rec up_to_nth_step (n:nat) (input:list eventval) (e:execution) (t:trace) : res (trace × state) ≝
     15let rec up_to_nth_step (n:nat) (input:list eventval) (e:execution state io_out io_in) (t:trace) : res (trace × state) ≝
    1616match n with
    1717[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? 〈t⧺tr, s〉
Note: See TracChangeset for help on using the changeset viewer.