summaryrefslogtreecommitdiff
path: root/Test/extractloops/t2.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/extractloops/t2.bpl')
-rw-r--r--Test/extractloops/t2.bpl108
1 files changed, 54 insertions, 54 deletions
diff --git a/Test/extractloops/t2.bpl b/Test/extractloops/t2.bpl
index d62733f7..39d65292 100644
--- a/Test/extractloops/t2.bpl
+++ b/Test/extractloops/t2.bpl
@@ -1,54 +1,54 @@
-// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var g: int;
-
-
-procedure foo()
-{
- var t: int;
- t := 0;
-}
-
-procedure {:entrypoint} A()
-modifies g;
-{
- var x: int;
- var y: int;
-
- anon0:
- assume g == 0;
- x := 4;
- goto anon3_LoopHead;
-
- anon3_LoopHead:
- call foo();
- goto anon3_LoopDone, anon3_LoopBody;
-
- anon3_LoopBody:
- assume g < x;
- g := g + 1;
- x := x - 1;
- y := 0;
- goto lab1_LoopHead;
-
- lab1_LoopHead:
- goto lab1_LoopBody, lab1_LoopDone;
-
- lab1_LoopBody:
- assume y < 2;
- y := y + 1;
- goto lab1_LoopHead;
-
- lab1_LoopDone:
- assume y >= 2;
- goto anon3_LoopHead;
-
- anon3_LoopDone:
- assume g >= x;
- goto anon2;
-
- anon2:
- return;
-}
-
-
+// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var g: int;
+
+
+procedure foo()
+{
+ var t: int;
+ t := 0;
+}
+
+procedure {:entrypoint} A()
+modifies g;
+{
+ var x: int;
+ var y: int;
+
+ anon0:
+ assume g == 0;
+ x := 4;
+ goto anon3_LoopHead;
+
+ anon3_LoopHead:
+ call foo();
+ goto anon3_LoopDone, anon3_LoopBody;
+
+ anon3_LoopBody:
+ assume g < x;
+ g := g + 1;
+ x := x - 1;
+ y := 0;
+ goto lab1_LoopHead;
+
+ lab1_LoopHead:
+ goto lab1_LoopBody, lab1_LoopDone;
+
+ lab1_LoopBody:
+ assume y < 2;
+ y := y + 1;
+ goto lab1_LoopHead;
+
+ lab1_LoopDone:
+ assume y >= 2;
+ goto anon3_LoopHead;
+
+ anon3_LoopDone:
+ assume g >= x;
+ goto anon2;
+
+ anon2:
+ return;
+}
+
+