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/stratifiedinline/bar6.bpl | |
parent | d7fc0deb2ca6d7ebee094b6ea5430d9b41f163ec (diff) |
Merging complete. Everything looks good *crosses fingers*
Diffstat (limited to 'Test/stratifiedinline/bar6.bpl')
-rw-r--r-- | Test/stratifiedinline/bar6.bpl | 76 |
1 files changed, 38 insertions, 38 deletions
diff --git a/Test/stratifiedinline/bar6.bpl b/Test/stratifiedinline/bar6.bpl index d763a82c..68c1faac 100644 --- a/Test/stratifiedinline/bar6.bpl +++ b/Test/stratifiedinline/bar6.bpl @@ -1,38 +1,38 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var M: [int]int;
-
-procedure bar(y: int) returns (b: bool)
-modifies M;
-{
- if (b) {
- M[y] := M[y] + 1;
- } else {
- M[y] := M[y] - 1;
- }
-}
-
-procedure foo(x: int, y: int)
-modifies M;
-{
- var b: bool;
-
- call b := bar(y);
- if (b) {
- M[x] := M[x] + 1;
- } else {
- M[x] := M[x] - 1;
- }
-}
-
-procedure {:entrypoint} main(x: int, y: int) returns (b: bool)
-modifies M;
-{
- assume x != y;
- assume M[x] == M[y];
- call foo(x, y);
- if (M[x] == M[y]) {
- call b := bar(y);
- assume (if b then M[x]+1 != M[y] else M[x] != M[y]+1);
- }
-}
+// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var M: [int]int; + +procedure bar(y: int) returns (b: bool) +modifies M; +{ + if (b) { + M[y] := M[y] + 1; + } else { + M[y] := M[y] - 1; + } +} + +procedure foo(x: int, y: int) +modifies M; +{ + var b: bool; + + call b := bar(y); + if (b) { + M[x] := M[x] + 1; + } else { + M[x] := M[x] - 1; + } +} + +procedure {:entrypoint} main(x: int, y: int) returns (b: bool) +modifies M; +{ + assume x != y; + assume M[x] == M[y]; + call foo(x, y); + if (M[x] == M[y]) { + call b := bar(y); + assume (if b then M[x]+1 != M[y] else M[x] != M[y]+1); + } +} |