Changeset 2391 for src/Clight/test/controlflow.c.ma

Timestamp:

Oct 9, 2012, 3:10:07 PM (8 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:

• src/Clight/test/controlflow.c.ma (modified) (2 diffs)

src/Clight/test/controlflow.c.ma

@@ -28 +28 @@
                (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
                (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
-               (Tint I32 Signed  ))))
-         (None ?))
+               (Tint I32 Signed  )))))
          (Ssequence
          (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
@@ -133 +132 @@
                  (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
                  (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
-                 (Tint I32 Signed  )))))
-             (None ?)))
+                 (Tint I32 Signed  )))))))
          )
          (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))