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


Ignore:
Timestamp:
May 13, 2011, 1:10:23 PM (10 years ago)
Author:
campbell
Message:

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File:
1 edited

Legend:

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

    r731 r797  
    2323example exec:
    2424 (do r ← exec_up_to clight_fullexec myprog 1000 [EVint (repr 7)];
    25   match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? ]) =
     25  match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? [ ] ]) =
    2626 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
    2727normalize  (* you can examine the result here *)
Note: See TracChangeset for help on using the changeset viewer.