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/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));
Note: See TracChangeset for help on using the changeset viewer.