From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Jun 2015 01:44:30 +0100 Subject: Normalise line endings using a .gitattributes file. Unfortunately this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. --- Test/extractloops/detLoopExtract.bpl | 4 +- Test/extractloops/t1.bpl | 86 ++++++++++++++-------------- Test/extractloops/t2.bpl | 108 +++++++++++++++++------------------ Test/extractloops/t3.bpl | 86 ++++++++++++++-------------- 4 files changed, 142 insertions(+), 142 deletions(-) (limited to 'Test/extractloops') diff --git a/Test/extractloops/detLoopExtract.bpl b/Test/extractloops/detLoopExtract.bpl index 7e9d0629..463cecf0 100644 --- a/Test/extractloops/detLoopExtract.bpl +++ b/Test/extractloops/detLoopExtract.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -deterministicExtractLoops -recursionBound:4 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -deterministicExtractLoops -recursionBound:4 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" var g:int; var h:int; //not modified var k:int; //modified in a procedure call diff --git a/Test/extractloops/t1.bpl b/Test/extractloops/t1.bpl index a0ebb0b8..731c4e44 100644 --- a/Test/extractloops/t1.bpl +++ b/Test/extractloops/t1.bpl @@ -1,43 +1,43 @@ -// 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; - goto anon3_LoopHead; - - anon3_LoopDone: - assume g >= x; - goto anon2; - - anon2: - assume x != 1; - 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; + goto anon3_LoopHead; + + anon3_LoopDone: + assume g >= x; + goto anon2; + + anon2: + assume x != 1; + return; +} + + 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; +} + + 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