Changeset 2391 for src/Clight/Csyntax.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/Csyntax.ma

    r2353 r2391  
    194194  | Ssequence : statement → statement → statement  (**r sequence *)
    195195  | Sifthenelse : expr  → statement → statement → statement (**r conditional *)
    196   | Swhile : expr → statement → option costlabel → statement   (**r [while] loop *)
     196  | Swhile : expr → statement → statement   (**r [while] loop *)
    197197  | Sdowhile : expr → statement → statement (**r [do] loop *)
    198198  | Sfor: statement → expr → statement → statement → statement (**r [for] loop *)
     
    226226  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    227227  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    228   (Swh:∀e,s,l. P s → P (Swhile e s l))
     228  (Swh:∀e,s. P s → P (Swhile e s))
    229229  (Sdo:∀e,s. P s → P (Sdowhile e s))
    230230  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     
    249249    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    250250    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    251 | Swhile e s cl ⇒ Swh e s cl
     251| Swhile e s ⇒ Swh e s
    252252    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    253253| Sdowhile e s ⇒ Sdo e s
     
    275275  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    276276  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    277   (Swh:∀e,s,l. P s → P (Swhile e s l))
     277  (Swh:∀e,s. P s → P (Swhile e s))
    278278  (Sdo:∀e,s. P s → P (Sdowhile e s))
    279279  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
Note: See TracChangeset for help on using the changeset viewer.