Changeset 2391 for src/Clight/label.ma


Ignore:
Timestamp:
Oct 9, 2012, 3:10:07 PM (7 years ago)
Author:
campbell
Message:

Revert "Put the post-loop cost label into the Clight while statement ..."
Rely on the Cminor to RTLabs stage ignoring Cminor skips instead.
This reverts commit 2353.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r2353 r2391  
    2727| Ssequence s1 s2 ⇒ statement_label_free s1 ∧ statement_label_free s2
    2828| Sifthenelse e1 s1 s2 ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ statement_label_free s2
    29 | Swhile e1 s1 cl ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ match cl with [ None ⇒ true | _ ⇒ false ]
     29| Swhile e1 s1 ⇒ expr_label_free e1 ∧ statement_label_free s1
    3030| Sdowhile e1 s1 ⇒ expr_label_free e1 ∧ statement_label_free s1
    3131| Sfor s1 e1 s2 s3 ⇒ statement_label_free s1 ∧ expr_label_free e1 ∧ statement_label_free s2 ∧ statement_label_free s3
     
    145145| Some e ⇒ let 〈e,costgen〉 ≝ label_expr e costgen in 〈Some ? e,costgen〉
    146146].
    147 
    148 definition ensure_label : option costlabel → universe CostTag → costlabel × (universe CostTag) ≝
    149 λo,u.
    150   match o with
    151   [ Some cl ⇒ 〈cl,u〉
    152   | None ⇒ fresh … u
    153   ].
    154147
    155148
     
    178171    let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in
    179172    〈Sifthenelse e s1 s2, costgen〉
    180 | Swhile e s' cl
     173| Swhile e s'
    181174    let 〈e,costgen〉 ≝ label_expr e costgen in
    182175    let 〈s',costgen〉 ≝ label_statement s' costgen in
    183176    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
    184     let 〈after,costgen〉 ≝ ensure_label cl costgen in
    185     〈Swhile e s' (Some ? after), costgen〉
     177    let 〈s,costgen〉 ≝ add_cost_after (Swhile e s') costgen in
     178    〈s,costgen〉
    186179| Sdowhile e s' ⇒
    187180    let 〈e,costgen〉 ≝ label_expr e costgen in
Note: See TracChangeset for help on using the changeset viewer.