diff options
Diffstat (limited to 'Test/extractloops/t3.bpl')
-rw-r--r-- | Test/extractloops/t3.bpl | 86 |
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; +} + + |