Changeset 2319 for src/compiler.ma


Ignore:
Timestamp:
Sep 3, 2012, 1:16:29 PM (7 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/compiler.ma

    r2291 r2319  
    77include "Cminor/toRTLabs.ma".
    88
    9 definition front_end : clight_program → res (clight_program × RTLabs_program) ≝
     9definition front_end : clight_program → res (costlabel × clight_program × RTLabs_program) ≝
    1010λp.
    11   let p' ≝ clight_label p in
     11  let 〈p',init_cost〉 ≝ clight_label p in
    1212  let p ≝ simplify_program p' in
    1313(*  let p ≝ program_switch_removal p in*)
    1414  ! p ← clight_to_cminor p;
    15   let p ≝ cminor_to_rtlabs p in
    16   return 〈p',p〉.
     15  let p ≝ cminor_to_rtlabs init_cost p in
     16  return 〈init_cost,p',p〉.
    1717
    1818include "RTLabs/RTLabsToRTL.ma".
Note: See TracChangeset for help on using the changeset viewer.