Changeset 731 for src/Clight/test/io.ma


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/io.ma

    r726 r731  
    1 include "Clight/Animation.ma".
     1include "Clight/Cexec.ma".
     2include "common/Animation.ma".
    23
    34definition myprog := mk_program clight_fundef type
     
    2122
    2223example exec:
    23  (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 7)]; do r ← opt_to_res … (is_final s); OK ? 〈t,r〉) =
     24 (do r ← exec_up_to clight_fullexec myprog 1000 [EVint (repr 7)];
     25  match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? ]) =
    2426 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
    2527normalize  (* you can examine the result here *)
Note: See TracChangeset for help on using the changeset viewer.