Changeset 781
 Timestamp:
 Apr 28, 2011, 4:43:50 PM (10 years ago)
 Location:
 src
 Files:

 1 added
 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/test/insertsort.ma
r731 r781 214 214 @refl 215 215 qed. 216 217 include "Clight/label.ma". 218 219 example labelled_exec: 220 (do p ← clight_label myprog; 221 do s ← exec_up_to clight_fullexec p 1000 222 [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 ? 224 [EVextcall (ident_of_nat 11) [EVint (repr 36)] (EVint (repr 0)); 225 EVextcall (ident_of_nat 11) [EVint (repr 69)] (EVint (repr 0)); 226 EVextcall (ident_of_nat 11) [EVint (repr 102)] (EVint (repr 0)); 227 EVextcall (ident_of_nat 11) [EVint (repr 105)] (EVint (repr 0)); 228 EVextcall (ident_of_nat 11) [EVint (repr 136)] (EVint (repr 0)); 229 EVextcall (ident_of_nat 11) [EVint (repr 234)] (EVint (repr 0)); 230 EVextcall (ident_of_nat 11) [EVint (repr 240)] (EVint (repr 0))] 231 . 232 normalize (* you can examine the result here *) 233 @refl 234 qed. 
src/common/Events.ma
r720 r781 70 70 ]. 71 71 72 (* Useful for testing programs. *) 73 definition remove_costs : trace → trace ≝ 74 filter … (λe. match e with [ EVcost _ ⇒ false  _ ⇒ true ]). 75 72 76 (* * Concatenation of traces is written [**] in the finite case 73 77 or [***] in the infinite case. *)
Note: See TracChangeset
for help on using the changeset viewer.