Changeset 797 for src/Clight/test


Ignore:
Timestamp:
May 13, 2011, 1:10:23 PM (9 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.

Location:
src/Clight/test
Files:
3 edited

Legend:

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

    r781 r797  
    202202  (do s ← exec_up_to clight_fullexec myprog 1000
    203203     [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 ?
     204   match s with [ finished t _ _ ⇒ OK ? t | _ ⇒ Error ? [ ] ]) = OK ?
    205205[EVextcall (ident_of_nat 11) [EVint (repr 36)] (EVint (repr 0));
    206206 EVextcall (ident_of_nat 11) [EVint (repr 69)] (EVint (repr 0));
     
    221221   do s ← exec_up_to clight_fullexec p 1000
    222222     [EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0)];
    223    match s with [ finished t _ _ ⇒ OK ? (remove_costs t) | _ ⇒ Error ? ]) = OK ?
     223   match s with [ finished t _ _ ⇒ OK ? (remove_costs t) | _ ⇒ Error ? [ ] ]) = OK ?
    224224[EVextcall (ident_of_nat 11) [EVint (repr 36)] (EVint (repr 0));
    225225 EVextcall (ident_of_nat 11) [EVint (repr 69)] (EVint (repr 0));
  • 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 *)
  • src/Clight/test/io2.ma

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