summaryrefslogtreecommitdiff
path: root/Test/test2/Structured.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test2/Structured.bpl')
-rw-r--r--Test/test2/Structured.bpl692
1 files changed, 346 insertions, 346 deletions
diff --git a/Test/test2/Structured.bpl b/Test/test2/Structured.bpl
index 55ee847a..a5aebaa9 100644
--- a/Test/test2/Structured.bpl
+++ b/Test/test2/Structured.bpl
@@ -1,346 +1,346 @@
-// RUN: %boogie -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-const K: int;
-
-function f(int) returns (int);
-
-axiom (exists k: int :: f(k) == K);
-
-procedure Find(a: int, b: int) returns (k: int);
- requires a <= b && (forall j: int :: a < j && j < b ==> f(j) != K);
- ensures f(k) == K;
-
-// nondeterministic, unstructured, recursive version
-implementation Find(a: int, b: int) returns (k: int)
-{
- entry:
- goto A, B, C;
-
- A:
- assume f(a) == K;
- k := a;
- return;
-
- B:
- assume f(b) == K;
- k := b;
- return;
-
- C:
- assume f(a) != K && f(b) != K;
- call k := Find(a-1, b+1);
- return;
-}
-
-// nondeterministic, recursive version
-implementation Find(a: int, b: int) returns (k: int)
-{
- if (*) {
- assume f(a) == K;
- k := a;
- } else if (*) {
- assume f(b) == K;
- k := b;
- } else {
- assume f(a) != K && f(b) != K;
- call k := Find(a-1, b+1);
- }
-}
-
-// deterministic, structured, recursive version
-implementation Find(a: int, b: int) returns (k: int)
-{
- if (f(a) == K) {
- k := a;
- } else if (f(b) == K) {
- k := b;
- } else {
- call k := Find(a-1, b+1);
- }
-}
-
-// deterministic, structured, iterative version
-implementation Find(a: int, b: int) returns (k: int)
-{
- var x: int, y: int;
-
- x := a;
- y := b;
-
- while (f(x) != K && f(y) != K)
- invariant x <= y && (forall j: int :: x < j && j < y ==> f(j) != K);
- {
- x := x-1;
- y := y+1;
- }
-
- if (f(x) == K) {
- k := x;
- } else {
- k := y;
- }
-}
-
-// deterministic, structured, iterative version with breaks
-implementation Find(a: int, b: int) returns (k: int)
-{
- var x: int, y: int;
-
- x := a;
- y := b;
-
- while (true)
- invariant x <= y && (forall j: int :: x < j && j < y ==> f(j) != K);
- {
- if (f(x) == K) {
- k := x;
- break;
- } else if (f(y) == K) {
- k := y;
- break;
- }
- x := x-1;
- y := y+1;
- }
-}
-
-// deterministic, somewhat structured, iterative version
-implementation Find(a: int, b: int) returns (k: int)
-{
- var x: int, y: int;
-
- x := a;
- y := b;
-
- while (true)
- invariant x <= y && (forall j: int :: x < j && j < y ==> f(j) != K);
- {
- if (f(x) == K) {
- goto FoundX;
- } else if (f(y) == K) {
- goto FoundY;
- }
- x := x-1;
- y := y+1;
- }
-
- FoundX:
- k := x;
- return;
-
- FoundY:
- k := y;
- return;
-}
-
-// deterministic, structured, iterative version with breaks
-implementation Find(a: int, b: int) returns (k: int)
-{
- var x: int, y: int;
-
- x := a;
- y := b;
-
- outer:
- if (true) {
- inner:
- while (true)
- invariant x <= y && (forall j: int :: x < j && j < y ==> f(j) != K);
- {
- if (f(x) == K) {
- break inner;
- } else if (f(y) == K) {
- break outer;
- }
- x := x-1;
- y := y+1;
- }
-
- k := x;
- return;
- }
- k := y;
-}
-
-// ----- free invariant -----
-
-function Teal(int) returns (bool);
-function ShadeOfGreen(int) returns (bool);
-axiom (forall w: int :: Teal(w) ==> ShadeOfGreen(w));
-
-procedure P(x: int) returns (y: int)
- requires Teal(x);
- ensures ShadeOfGreen(y);
-{
- y := x;
- while (y < 100)
- free invariant Teal(y);
- {
- y := y + 5;
- }
-}
-
-// ----- run off the end of the BigBlock -----
-
-procedure RunOffEnd0() returns (x: int)
- ensures x == 3;
-{
- x := 0;
- Label0:
- x := x + 1;
- Label1:
- x := x + 1;
- Label2:
- Label3:
- Label4:
- x := x + 1;
-}
-
-procedure RunOffEnd1() returns (x: int)
- ensures x == 4;
-{
- x := 0;
- Label0:
- x := x + 1;
- Label1:
- if (*) {
- Label2:
- x := x + 2;
- } else if (*) {
- Label3:
- x := 2;
- x := x + 2;
- Label4:
- Label5:
- x := x - 1;
- } else {
- if (*) {
- x := 0;
- while (x < 3)
- invariant x <= 3;
- { x := x + 1; }
- } else {
- x := x + 2;
- }
- }
- x := x + 1;
-}
-
-procedure RunOffEnd2() returns (x: int)
- ensures x == 10;
-{
- while (true) {
- while (true) {
- if (*) {
- x := 10;
- break;
- }
- }
- if (*) { break; }
- }
-}
-
-procedure RunOffEnd3() returns (x: int)
- ensures x == 9;
-{ x := 9;
- while (true) {
- while (true) {
- if (*) {
- x := 10;
- break;
- }
- }
- if (*) { break; }
- } // error: violated postcondition
-}
-
-procedure RunOffEnd4() returns (x: int)
-{
- var y: int;
- var bad: bool;
-
- while (true) {
- y := x;
- bad := false;
- if (*) {
- x := x + 1;
- bad := true;
- }
- if (x == y) { break; }
- }
- assert !bad;
-}
-
-procedure RunOffEnd5() returns (x: int)
-{
- while (true) {
- if (x == 5) { }
- }
- assert false;
-}
-
-procedure RunOffEnd6() returns (x: int)
-{
- x := 7;
- while (true)
- invariant x == 7;
- {
- x := 5;
- MyLabel:
- x := 7;
- }
-}
-
-// ----- jump optimizations -----
-
-procedure Q0()
-{
- var x: int;
-
- x := 0;
- if (*) {
- x := 1;
- }
- assert x == 1; // error
-}
-
-procedure Q1() returns (x: int)
-{
- if (x == 0) {
- A:
- x := x + 0;
- assert x == 0; // error
- B:
- x := x + 1;
- goto A;
- }
-}
-
-procedure Q2() returns (x: int)
-{
- if (x == 0) {
- while (x < 10)
- invariant x <= 10;
- {
- x := x + 1;
- }
- }
-}
-
-// There was once a bug in Boogie's handling of the following break statement.
-procedure BreakIssue(x: int) returns (curr: int)
- ensures x == 18 || curr == 100; // holds, because the procedure doesn't
- // actually ever terminate if x != 18
-{
- while (x != 18) {
- while (x != 19) {
- call curr := Read();
- if (curr == 0) {
- break;
- }
- }
- }
-}
-
-procedure Read() returns (val: int);
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+const K: int;
+
+function f(int) returns (int);
+
+axiom (exists k: int :: f(k) == K);
+
+procedure Find(a: int, b: int) returns (k: int);
+ requires a <= b && (forall j: int :: a < j && j < b ==> f(j) != K);
+ ensures f(k) == K;
+
+// nondeterministic, unstructured, recursive version
+implementation Find(a: int, b: int) returns (k: int)
+{
+ entry:
+ goto A, B, C;
+
+ A:
+ assume f(a) == K;
+ k := a;
+ return;
+
+ B:
+ assume f(b) == K;
+ k := b;
+ return;
+
+ C:
+ assume f(a) != K && f(b) != K;
+ call k := Find(a-1, b+1);
+ return;
+}
+
+// nondeterministic, recursive version
+implementation Find(a: int, b: int) returns (k: int)
+{
+ if (*) {
+ assume f(a) == K;
+ k := a;
+ } else if (*) {
+ assume f(b) == K;
+ k := b;
+ } else {
+ assume f(a) != K && f(b) != K;
+ call k := Find(a-1, b+1);
+ }
+}
+
+// deterministic, structured, recursive version
+implementation Find(a: int, b: int) returns (k: int)
+{
+ if (f(a) == K) {
+ k := a;
+ } else if (f(b) == K) {
+ k := b;
+ } else {
+ call k := Find(a-1, b+1);
+ }
+}
+
+// deterministic, structured, iterative version
+implementation Find(a: int, b: int) returns (k: int)
+{
+ var x: int, y: int;
+
+ x := a;
+ y := b;
+
+ while (f(x) != K && f(y) != K)
+ invariant x <= y && (forall j: int :: x < j && j < y ==> f(j) != K);
+ {
+ x := x-1;
+ y := y+1;
+ }
+
+ if (f(x) == K) {
+ k := x;
+ } else {
+ k := y;
+ }
+}
+
+// deterministic, structured, iterative version with breaks
+implementation Find(a: int, b: int) returns (k: int)
+{
+ var x: int, y: int;
+
+ x := a;
+ y := b;
+
+ while (true)
+ invariant x <= y && (forall j: int :: x < j && j < y ==> f(j) != K);
+ {
+ if (f(x) == K) {
+ k := x;
+ break;
+ } else if (f(y) == K) {
+ k := y;
+ break;
+ }
+ x := x-1;
+ y := y+1;
+ }
+}
+
+// deterministic, somewhat structured, iterative version
+implementation Find(a: int, b: int) returns (k: int)
+{
+ var x: int, y: int;
+
+ x := a;
+ y := b;
+
+ while (true)
+ invariant x <= y && (forall j: int :: x < j && j < y ==> f(j) != K);
+ {
+ if (f(x) == K) {
+ goto FoundX;
+ } else if (f(y) == K) {
+ goto FoundY;
+ }
+ x := x-1;
+ y := y+1;
+ }
+
+ FoundX:
+ k := x;
+ return;
+
+ FoundY:
+ k := y;
+ return;
+}
+
+// deterministic, structured, iterative version with breaks
+implementation Find(a: int, b: int) returns (k: int)
+{
+ var x: int, y: int;
+
+ x := a;
+ y := b;
+
+ outer:
+ if (true) {
+ inner:
+ while (true)
+ invariant x <= y && (forall j: int :: x < j && j < y ==> f(j) != K);
+ {
+ if (f(x) == K) {
+ break inner;
+ } else if (f(y) == K) {
+ break outer;
+ }
+ x := x-1;
+ y := y+1;
+ }
+
+ k := x;
+ return;
+ }
+ k := y;
+}
+
+// ----- free invariant -----
+
+function Teal(int) returns (bool);
+function ShadeOfGreen(int) returns (bool);
+axiom (forall w: int :: Teal(w) ==> ShadeOfGreen(w));
+
+procedure P(x: int) returns (y: int)
+ requires Teal(x);
+ ensures ShadeOfGreen(y);
+{
+ y := x;
+ while (y < 100)
+ free invariant Teal(y);
+ {
+ y := y + 5;
+ }
+}
+
+// ----- run off the end of the BigBlock -----
+
+procedure RunOffEnd0() returns (x: int)
+ ensures x == 3;
+{
+ x := 0;
+ Label0:
+ x := x + 1;
+ Label1:
+ x := x + 1;
+ Label2:
+ Label3:
+ Label4:
+ x := x + 1;
+}
+
+procedure RunOffEnd1() returns (x: int)
+ ensures x == 4;
+{
+ x := 0;
+ Label0:
+ x := x + 1;
+ Label1:
+ if (*) {
+ Label2:
+ x := x + 2;
+ } else if (*) {
+ Label3:
+ x := 2;
+ x := x + 2;
+ Label4:
+ Label5:
+ x := x - 1;
+ } else {
+ if (*) {
+ x := 0;
+ while (x < 3)
+ invariant x <= 3;
+ { x := x + 1; }
+ } else {
+ x := x + 2;
+ }
+ }
+ x := x + 1;
+}
+
+procedure RunOffEnd2() returns (x: int)
+ ensures x == 10;
+{
+ while (true) {
+ while (true) {
+ if (*) {
+ x := 10;
+ break;
+ }
+ }
+ if (*) { break; }
+ }
+}
+
+procedure RunOffEnd3() returns (x: int)
+ ensures x == 9;
+{ x := 9;
+ while (true) {
+ while (true) {
+ if (*) {
+ x := 10;
+ break;
+ }
+ }
+ if (*) { break; }
+ } // error: violated postcondition
+}
+
+procedure RunOffEnd4() returns (x: int)
+{
+ var y: int;
+ var bad: bool;
+
+ while (true) {
+ y := x;
+ bad := false;
+ if (*) {
+ x := x + 1;
+ bad := true;
+ }
+ if (x == y) { break; }
+ }
+ assert !bad;
+}
+
+procedure RunOffEnd5() returns (x: int)
+{
+ while (true) {
+ if (x == 5) { }
+ }
+ assert false;
+}
+
+procedure RunOffEnd6() returns (x: int)
+{
+ x := 7;
+ while (true)
+ invariant x == 7;
+ {
+ x := 5;
+ MyLabel:
+ x := 7;
+ }
+}
+
+// ----- jump optimizations -----
+
+procedure Q0()
+{
+ var x: int;
+
+ x := 0;
+ if (*) {
+ x := 1;
+ }
+ assert x == 1; // error
+}
+
+procedure Q1() returns (x: int)
+{
+ if (x == 0) {
+ A:
+ x := x + 0;
+ assert x == 0; // error
+ B:
+ x := x + 1;
+ goto A;
+ }
+}
+
+procedure Q2() returns (x: int)
+{
+ if (x == 0) {
+ while (x < 10)
+ invariant x <= 10;
+ {
+ x := x + 1;
+ }
+ }
+}
+
+// There was once a bug in Boogie's handling of the following break statement.
+procedure BreakIssue(x: int) returns (curr: int)
+ ensures x == 18 || curr == 100; // holds, because the procedure doesn't
+ // actually ever terminate if x != 18
+{
+ while (x != 18) {
+ while (x != 19) {
+ call curr := Read();
+ if (curr == 0) {
+ break;
+ }
+ }
+ }
+}
+
+procedure Read() returns (val: int);
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 07:10:31 +0000