Changeset 2724


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

Add RTLabs cost labelling checks to compiler.ma.

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostCheck.ma

    r2716 r2724  
    2525] qed.
    2626
    27 include alias "utilities/deqsets_extras.ma".
     27include alias "utilities/deqsets_extra.ma".
    2828
    2929lemma successors_present : ∀g,st.
     
    235235qed.
    236236
    237 include alias "utilities/deqsets_extras.ma".
     237include alias "utilities/deqsets_extra.ma".
    238238
    239239lemma after_branch_are_cost_labels : ∀g. ∀CL:graph_closed g.
  • src/RTLabs/RTLabs_abstract.ma

    r2716 r2724  
    1010include "common/StructuredTraces.ma".
    1111include "RTLabs/CostSpec.ma". (* TODO: relocate definitions? *)
    12 include "utilities/deqsets_extras.ma".
     12include "utilities/deqsets_extra.ma".
    1313discriminator status_class.
    1414
  • src/RTLabs/RTLabs_traces.ma

    r2716 r2724  
    23072307qed.
    23082308
    2309 include alias "utilities/deqsets_extras.ma".
     2309include alias "utilities/deqsets_extra.ma".
    23102310
    23112311(* Build the tail of the "bad" loop using the reappearance of the original pc,
  • src/common/ErrorMessages.ma

    r2668 r2724  
    6666 | OutOfBounds: ErrorMessage
    6767 | UnexpectedIO : ErrorMessage
    68  | TerminatedEarly : ErrorMessage.
     68 | TerminatedEarly : ErrorMessage
     69 | BadCostLabelling : ErrorMessage
     70 | RepeatedCostLabel : ErrorMessage.
  • 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.