From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Test/extractloops/t3.bpl | 86 ++++++++++++++++++++++++------------------------ 1 file changed, 43 insertions(+), 43 deletions(-) (limited to 'Test/extractloops/t3.bpl') 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; +} + + -- cgit v1.2.3