Changeset 781 for src/Clight/test


Ignore:
Timestamp:
Apr 28, 2011, 4:43:50 PM (9 years ago)
Author:
campbell
Message:

Implement labelling pass for Clight.

File:
1 edited

Legend:

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

    r731 r781  
    214214@refl
    215215qed.
     216
     217include "Clight/label.ma".
     218
     219example 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.
     232normalize  (* you can examine the result here *)
     233@refl
     234qed.
Note: See TracChangeset for help on using the changeset viewer.