diff options
Diffstat (limited to 'Test/aitest1/Answer')
| -rw-r--r-- | Test/aitest1/Answer | 510 |
1 files changed, 510 insertions, 0 deletions
diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer new file mode 100644 index 00000000..4e5c8f27 --- /dev/null +++ b/Test/aitest1/Answer @@ -0,0 +1,510 @@ +-------------------- ineq.bpl --------------------
+procedure SimpleLoop();
+
+
+
+implementation SimpleLoop()
+{
+ var i: int;
+
+ start:
+ assume true;
+ i := 0;
+ assume i == 0;
+ goto test;
+
+ test: // cut point
+ assume 0 <= i;
+ assume 0 <= i;
+ goto Then, Else;
+
+ Then:
+ assume 0 <= i;
+ assume i < 10;
+ i := i + 1;
+ assume i <= 10 && 1 <= i;
+ goto test;
+
+ Else:
+ assume 0 <= i;
+ assume !(i < 10);
+ assume 10 <= i;
+ return;
+}
+
+
+
+procedure VariableBoundLoop(n: int);
+
+
+
+implementation VariableBoundLoop(n: int)
+{
+ var i: int;
+
+ start:
+ assume true;
+ i := 0;
+ assume i == 0;
+ goto test;
+
+ test: // cut point
+ assume 0 <= i;
+ assume 0 <= i;
+ goto Then, Else;
+
+ Then:
+ assume 0 <= i;
+ assume i < n;
+ i := i + 1;
+ assume i <= n && 1 <= i;
+ goto test;
+
+ Else:
+ assume 0 <= i;
+ assume !(i < n);
+ assume n <= i && 0 <= i;
+ return;
+}
+
+
+
+procedure Foo();
+
+
+
+implementation Foo()
+{
+ var i: int;
+
+ start:
+ assume true;
+ i := 3 * i + 1;
+ i := 3 * (i + 1);
+ i := 1 + 3 * i;
+ i := (i + 1) * 3;
+ assume true;
+ return;
+}
+
+
+
+procedure FooToo();
+
+
+
+implementation FooToo()
+{
+ var i: int;
+
+ start:
+ assume true;
+ i := 5;
+ i := 3 * i + 1;
+ i := 3 * (i + 1);
+ i := 1 + 3 * i;
+ i := (i + 1) * 3;
+ assume 1 / 3 * i == 155;
+ return;
+}
+
+
+
+procedure FooTooStepByStep();
+
+
+
+implementation FooTooStepByStep()
+{
+ var i: int;
+
+ L0:
+ assume true;
+ i := 5;
+ assume i == 5;
+ goto L1;
+
+ L1:
+ assume i == 5;
+ i := 3 * i + 1;
+ assume i == 16;
+ goto L2;
+
+ L2:
+ assume i == 16;
+ i := 3 * (i + 1);
+ assume 1 / 3 * i == 17;
+ goto L3;
+
+ L3:
+ assume 1 / 3 * i == 17;
+ i := 1 + 3 * i;
+ assume i == 154;
+ goto L4;
+
+ L4:
+ assume i == 154;
+ i := (i + 1) * 3;
+ assume 1 / 3 * i == 155;
+ return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
+-------------------- Linear0.bpl --------------------
+var x: int;
+
+var y: int;
+
+procedure p();
+
+
+
+implementation p()
+{
+
+ start:
+ assume true;
+ assume true;
+ return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
+-------------------- Linear1.bpl --------------------
+var x: int;
+
+var y: int;
+
+procedure p();
+
+
+
+implementation p()
+{
+
+ start:
+ assume true;
+ assume x * x == y;
+ assume true;
+ return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
+-------------------- Linear2.bpl --------------------
+var x: int;
+
+var y: int;
+
+procedure p();
+
+
+
+implementation p()
+{
+
+ start:
+ assume true;
+ assume x == 8;
+ assume x == 8;
+ return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
+-------------------- Linear3.bpl --------------------
+var x: int;
+
+var y: int;
+
+procedure p();
+
+
+
+implementation p()
+{
+
+ start:
+ assume true;
+ assume x < y;
+ assume x + 1 <= y;
+ return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
+-------------------- Linear4.bpl --------------------
+var x: int;
+
+var y: int;
+
+procedure p();
+ modifies x;
+
+
+
+implementation p()
+{
+
+ A:
+ assume true;
+ assume x < y;
+ assume x + 1 <= y;
+ goto B;
+
+ B:
+ assume x + 1 <= y;
+ x := x * x;
+ assume true;
+ return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
+-------------------- Linear5.bpl --------------------
+var x: int;
+
+var y: int;
+
+procedure p();
+ modifies x;
+
+
+
+implementation p()
+{
+
+ A:
+ assume true;
+ assume 0 - 1 <= x;
+ assume -1 <= x;
+ goto B;
+
+ B:
+ assume -1 <= x;
+ assume x < y;
+ assume x + 1 <= y && -1 <= x;
+ goto C;
+
+ C:
+ assume x + 1 <= y && -1 <= x;
+ x := x * x;
+ assume 0 <= y;
+ goto D;
+
+ D:
+ assume 0 <= y;
+ x := y;
+ assume x == y && 0 <= y;
+ return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
+-------------------- Linear6.bpl --------------------
+var x: int;
+
+var y: int;
+
+var z: int;
+
+procedure p();
+ modifies x;
+
+
+
+implementation p()
+{
+
+ A:
+ assume true;
+ x := 8;
+ assume x == 8;
+ goto B, C;
+
+ B:
+ assume x == 8;
+ x := 9;
+ assume x == 9;
+ goto D;
+
+ C:
+ assume x == 8;
+ x := 10;
+ assume x == 10;
+ goto D;
+
+ D:
+ assume 9 <= x && x <= 10;
+ assume 9 <= x && x <= 10;
+ return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
+-------------------- Linear7.bpl --------------------
+var x: int;
+
+var y: int;
+
+var z: int;
+
+procedure p();
+
+
+
+implementation p()
+{
+
+ A:
+ assume true;
+ assume true;
+ goto B, C;
+
+ B:
+ assume true;
+ assume x <= 0;
+ assume x <= 0;
+ goto D;
+
+ C:
+ assume true;
+ assume y <= 0;
+ assume y <= 0;
+ goto D;
+
+ D:
+ assume true;
+ assume true;
+ return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
+-------------------- Linear8.bpl --------------------
+procedure foo();
+
+
+
+implementation foo()
+{
+ var i: int;
+ var j: int;
+ var n: int;
+
+ A:
+ assume true;
+ n := 0;
+ assume n == 0;
+ goto B;
+
+ B:
+ assume n == 0;
+ j := 0;
+ assume j == 0 && n == 0;
+ goto C;
+
+ C:
+ assume j == 0 && n == 0;
+ i := j + 1;
+ assume i == j + 1 && j == 0 && n == 0;
+ goto D;
+
+ D:
+ assume i == j + 1 && j == 0 && n == 0;
+ i := i + 1;
+ assume i == j + 2 && j == 0 && n == 0;
+ goto E;
+
+ E:
+ assume i == j + 2 && j == 0 && n == 0;
+ i := i + 1;
+ assume i == j + 3 && j == 0 && n == 0;
+ goto F;
+
+ F:
+ assume i == j + 3 && j == 0 && n == 0;
+ i := i + 1;
+ assume i == j + 4 && j == 0 && n == 0;
+ goto G;
+
+ G:
+ assume i == j + 4 && j == 0 && n == 0;
+ i := i + 1;
+ assume i == j + 5 && j == 0 && n == 0;
+ goto H;
+
+ H:
+ assume i == j + 5 && j == 0 && n == 0;
+ j := j + 1;
+ assume i == j + 4 && j == 1 && n == 0;
+ goto I;
+
+ I:
+ assume i == j + 4 && j == 1 && n == 0;
+ assume i == j + 4 && j == 1 && n == 0;
+ return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
+-------------------- Linear9.bpl --------------------
+procedure foo();
+
+
+
+implementation foo()
+{
+ var i: int;
+ var j: int;
+ var n: int;
+
+ entry:
+ assume true;
+ assume n >= 4;
+ i := 0;
+ j := i + 1;
+ assume j == i + 1 && i == 0 && 4 <= n;
+ goto exit, loop0;
+
+ loop0: // cut point
+ assume 4 <= n && 0 <= i && j == i + 1;
+ assume j <= n;
+ assume j <= n && 4 <= n && 0 <= i && j == i + 1;
+ goto loop1;
+
+ loop1:
+ assume j <= n && 4 <= n && 0 <= i && j == i + 1;
+ i := i + 1;
+ assume 1 <= i && j == i && j <= n && 4 <= n;
+ goto loop2;
+
+ loop2:
+ assume j <= n && 4 <= n && 1 <= i && j == i;
+ j := j + 1;
+ assume j <= n + 1 && j == i + 1 && 4 <= n && 1 <= i;
+ goto loop0, exit;
+
+ exit:
+ assume j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;
+ assume j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;
+ return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
+-------------------- Bound.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
|