summaryrefslogtreecommitdiff
path: root/Test/extractloops/t3.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/extractloops/t3.bpl')
-rw-r--r--Test/extractloops/t3.bpl86
1 files changed, 43 insertions, 43 deletions
diff --git a/Test/extractloops/t3.bpl b/Test/extractloops/t3.bpl
index 023a9adb..9e7720ec 100644
--- a/Test/extractloops/t3.bpl
+++ b/Test/extractloops/t3.bpl
@@ -1,43 +1,43 @@
-// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -recursionBound:2 "%s" > "%t"
-// RUN: %diff "%s.rb2.expect" "%t"
-// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -recursionBound:4 "%s" > "%t"
-// RUN: %diff "%s.rb4.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_LoopBody;
-
- anon3_LoopHead:
- call foo();
- goto anon3_LoopDone, anon3_LoopBody;
-
- anon3_LoopBody:
- assume g < x;
- g := g + 1;
- x := x - 1;
- goto anon3_LoopHead;
-
- anon3_LoopDone:
- assume g >= x;
- goto anon2;
-
- anon2:
- assume x != 1;
- return;
-}
-
-
+// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -recursionBound:2 "%s" > "%t"
+// RUN: %diff "%s.rb2.expect" "%t"
+// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -recursionBound:4 "%s" > "%t"
+// RUN: %diff "%s.rb4.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_LoopBody;
+
+ anon3_LoopHead:
+ call foo();
+ goto anon3_LoopDone, anon3_LoopBody;
+
+ anon3_LoopBody:
+ assume g < x;
+ g := g + 1;
+ x := x - 1;
+ goto anon3_LoopHead;
+
+ anon3_LoopDone:
+ assume g >= x;
+ goto anon2;
+
+ anon2:
+ assume x != 1;
+ return;
+}
+
+