diff options
Diffstat (limited to 'Test/inline/InliningAndLoops.bpl')
-rw-r--r-- | Test/inline/InliningAndLoops.bpl | 44 |
1 files changed, 22 insertions, 22 deletions
diff --git a/Test/inline/InliningAndLoops.bpl b/Test/inline/InliningAndLoops.bpl index 74b20913..52901480 100644 --- a/Test/inline/InliningAndLoops.bpl +++ b/Test/inline/InliningAndLoops.bpl @@ -1,22 +1,22 @@ -// RUN: %boogie -loopUnroll:3 -soundLoopUnrolling "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure foo(N: int)
- requires N == 2;
-{
- var n, sum, recent: int;
- n, sum := 0, 0;
- while (n < N)
- {
- call recent := bar();
- sum, n := sum + recent, n + 1;
- }
- if (n == 2) {
- assert sum == recent + recent; // no reason to believe this always to be true
- }
-}
-
-procedure {:inline 1} bar() returns (r: int)
-{
- var x: int;
- r := x;
-}
+// RUN: %boogie -loopUnroll:3 -soundLoopUnrolling "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo(N: int) + requires N == 2; +{ + var n, sum, recent: int; + n, sum := 0, 0; + while (n < N) + { + call recent := bar(); + sum, n := sum + recent, n + 1; + } + if (n == 2) { + assert sum == recent + recent; // no reason to believe this always to be true + } +} + +procedure {:inline 1} bar() returns (r: int) +{ + var x: int; + r := x; +} |