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/t2.bpl | 108 +++++++++++++++++++++++------------------------ 1 file changed, 54 insertions(+), 54 deletions(-) (limited to 'Test/extractloops/t2.bpl') 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; +} + + -- cgit v1.2.3