Changeset 2353 for src/Clight/Cexec.ma


Ignore:
Timestamp:
Sep 26, 2012, 6:14:38 PM (7 years ago)
Author:
campbell
Message:

Put the post-loop cost label into the Clight while statement to get rid
of extra skips. (Soon to be followed by other loop constructs.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r2203 r2353  
    390390          | _ ⇒ Wrong ??? (msg NonsenseState)
    391391          ]
    392       | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
     392      | Kwhile a s' cl k' ⇒ ret ? 〈E0, State f (Swhile a s' cl) k' e m〉
    393393      | Kdowhile a s' k' ⇒
    394394          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
     
    406406      match k with
    407407      [ Kseq s' k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
    408       | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
     408      | Kwhile a s' cl k' ⇒ ret ? 〈E0, State f (Swhile a s' cl) k' e m〉
    409409      | Kdowhile a s' k' ⇒
    410410          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
     
    421421      match k with
    422422      [ Kseq s' k' ⇒ ret ? 〈E0, State f Sbreak k' e m〉
    423       | Kwhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
     423      | Kwhile a s' cl k' ⇒ ret ? 〈E0, State f (optional_cost cl Sskip) k' e m〉
    424424      | Kdowhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
    425425      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
     
    431431      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    432432      ret ? 〈tr, State f (if b then s1 else s2) k e m〉
    433   | Swhile a s'
     433  | Swhile a s' cl
    434434      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    435435      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    436       ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
    437                       else State f Sskip k e m〉
     436      ret ? 〈tr, if b then State f s' (Kwhile a s' cl k) e m
     437                      else State f (optional_cost cl Sskip) k e m〉
    438438  | Sdowhile a s' ⇒ ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉
    439439  | Sfor a1 a2 a3 s' ⇒
Note: See TracChangeset for help on using the changeset viewer.