Ignore:
Timestamp:
Apr 1, 2011, 1:35:18 PM (9 years ago)
Author:
campbell
Message:

Common definition for animation semantics, and factor out IO definitions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/insertsort.ma

    r726 r731  
    1 include "Clight/Animation.ma".
     1include "Clight/Cexec.ma".
     2include "common/Animation.ma".
    23
    34definition myprog := mk_program clight_fundef type
     
    199200
    200201example exec:
    201   (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0)];
    202    OK ? t) = OK ?
     202  (do s ← exec_up_to clight_fullexec myprog 1000
     203     [EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0)];
     204   match s with [ finished t _ _ ⇒ OK ? t | _ ⇒ Error ? ]) = OK ?
    203205[EVextcall (ident_of_nat 11) [EVint (repr 36)] (EVint (repr 0));
    204206 EVextcall (ident_of_nat 11) [EVint (repr 69)] (EVint (repr 0));
Note: See TracChangeset for help on using the changeset viewer.