Changeset 2724 for src/compiler.ma


Ignore:
Timestamp:
Feb 24, 2013, 8:39:19 PM (7 years ago)
Author:
campbell
Message:

Add RTLabs cost labelling checks to compiler.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2709 r2724  
    55include "Cminor/initialisation.ma".
    66include "Cminor/toRTLabs.ma".
     7include "RTLabs/CostCheck.ma".
     8include "RTLabs/CostInj.ma".
    79
    810definition front_end : clight_program → res (costlabel × clight_program × RTLabs_program) ≝
     
    1315  ! p ← clight_to_cminor p;
    1416  let p ≝ cminor_to_rtlabs init_cost p in
    15   return 〈init_cost,p',p〉.
     17  if check_cost_program p then
     18    if check_program_cost_injectivity p then
     19      (return 〈init_cost,p',p〉)
     20    else
     21      (Error ? (msg RepeatedCostLabel))
     22  else
     23    (Error ? (msg BadCostLabelling)).
    1624
    1725include "RTLabs/RTLabsToRTL.ma".
Note: See TracChangeset for help on using the changeset viewer.