Changeset 781


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

Implement labelling pass for Clight.

Location:
src
Files:
1 added
2 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.
  • src/common/Events.ma

    r720 r781  
    7070  ].
    7171
     72(* Useful for testing programs. *)
     73definition remove_costs : trace → trace ≝
     74filter … (λe. match e with [ EVcost _ ⇒ false | _ ⇒ true ]).
     75
    7276(* * Concatenation of traces is written [**] in the finite case
    7377  or [***] in the infinite case. *)
Note: See TracChangeset for help on using the changeset viewer.