Ignore:
Timestamp:
Sep 3, 2012, 1:16:29 PM (8 years ago)
Author:
campbell
Message:

Generate per-program cost labels rather than per-function ones, and
produce an extra cost label for the global variable initialisation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSpecification.ma

    r2202 r2319  
    3232∀p:clight_program.
    3333  let e1 ≝ exec_inf … clight_fullexec p in
    34   let e2 ≝ exec_inf … clight_fullexec (clight_label p) in
     34  let e2 ≝ exec_inf … clight_fullexec (\fst (clight_label p)) in
    3535  not_wrong state e1 →
    3636  sim_with_labels e1 e2.
Note: See TracChangeset for help on using the changeset viewer.