diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
commit | d652155ae013f36a1ee17653a8e458baad2d9c2c (patch) | |
tree | 067d600fe3cd1723afc11682935f0123a1eab653 /Test/inline/InliningAndLoops.bpl | |
parent | d7fc0deb2ca6d7ebee094b6ea5430d9b41f163ec (diff) |
Merging complete. Everything looks good *crosses fingers*
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; +} |