Initial set of files.

author: mikebarnett <unknown> 2009-07-15 21:03:41 +0000
committer: mikebarnett <unknown> 2009-07-15 21:03:41 +0000
commit: ce1c2de044c91624370411e23acab13b0381949b (patch)
tree: 592539996fe08050ead5ee210c973801611dde40 /Test/aitest1
15 files changed, 1336 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
diff --git a/Test/aitest1/Bound.bpl b/Test/aitest1/Bound.bpl
new file mode 100644
index 00000000..02b2c460
--- /dev/null
+++ b/Test/aitest1/Bound.bpl
@@ -0,0 +1,28 @@
+const TEST: name;
+
+procedure P()
+{
+var i: int;
+var N: int;
+
+start:
+  assume N >= 0;
+  i := 0;
+  assert i <= N;
+  goto LoopHead;
+
+LoopHead:
+  goto LoopBody, AfterLoop;
+
+LoopBody:
+  assume i < N;
+  i := i + 1;
+  goto LoopHead;
+
+AfterLoop:
+  assume !(i < N);
+  assert i == N;
+  return;
+}
+
+type name;
+\ No newline at end of file
diff --git a/Test/aitest1/Linear0.bpl b/Test/aitest1/Linear0.bpl
new file mode 100644
index 00000000..7a11c803
--- /dev/null
+++ b/Test/aitest1/Linear0.bpl
@@ -0,0 +1,10 @@
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+
+procedure p()
+{
+  start:
+    return;
+}
diff --git a/Test/aitest1/Linear1.bpl b/Test/aitest1/Linear1.bpl
new file mode 100644
index 00000000..0cbb4a07
--- /dev/null
+++ b/Test/aitest1/Linear1.bpl
@@ -0,0 +1,11 @@
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+
+procedure p()
+{
+  start:
+    assume x*x == y;  // not a linear condition
+    return;
+}
diff --git a/Test/aitest1/Linear2.bpl b/Test/aitest1/Linear2.bpl
new file mode 100644
index 00000000..9e02c9e2
--- /dev/null
+++ b/Test/aitest1/Linear2.bpl
@@ -0,0 +1,11 @@
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+
+procedure p()
+{
+  start:
+    assume x == 8;
+    return;
+}
diff --git a/Test/aitest1/Linear3.bpl b/Test/aitest1/Linear3.bpl
new file mode 100644
index 00000000..c6b7a441
--- /dev/null
+++ b/Test/aitest1/Linear3.bpl
@@ -0,0 +1,11 @@
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+
+procedure p()
+{
+  start:
+    assume x < y;
+    return;
+}
diff --git a/Test/aitest1/Linear4.bpl b/Test/aitest1/Linear4.bpl
new file mode 100644
index 00000000..c8c4605c
--- /dev/null
+++ b/Test/aitest1/Linear4.bpl
@@ -0,0 +1,15 @@
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+
+procedure p()
+  modifies x;
+{
+  A:
+    assume x < y;
+    goto B;
+  B:
+    x := x*x;
+    return;
+}
diff --git a/Test/aitest1/Linear5.bpl b/Test/aitest1/Linear5.bpl
new file mode 100644
index 00000000..4f04999c
--- /dev/null
+++ b/Test/aitest1/Linear5.bpl
@@ -0,0 +1,21 @@
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+
+procedure p()
+  modifies x;
+{
+  A:
+    assume -1 <= x;
+    goto B;
+  B:
+    assume x < y;
+    goto C;
+  C:
+    x := x*x;
+    goto D;
+  D:
+    x := y;
+    return;
+}
diff --git a/Test/aitest1/Linear6.bpl b/Test/aitest1/Linear6.bpl
new file mode 100644
index 00000000..83e52a9a
--- /dev/null
+++ b/Test/aitest1/Linear6.bpl
@@ -0,0 +1,21 @@
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+var z: int;
+
+procedure p()
+  modifies x;
+{
+A:
+    x := 8;
+    goto B, C;
+B:
+    x := 9;
+    goto D;
+C:
+    x := 10;
+    goto D;
+D:
+    return;
+}
diff --git a/Test/aitest1/Linear7.bpl b/Test/aitest1/Linear7.bpl
new file mode 100644
index 00000000..b1bcaaaf
--- /dev/null
+++ b/Test/aitest1/Linear7.bpl
@@ -0,0 +1,19 @@
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+var z: int;
+
+procedure p()
+{
+A:
+    goto B, C;
+B:
+    assume x <= 0;
+    goto D;
+C:
+    assume y <= 0;
+    goto D;
+D:
+    return;
+}
diff --git a/Test/aitest1/Linear8.bpl b/Test/aitest1/Linear8.bpl
new file mode 100644
index 00000000..4bc3f887
--- /dev/null
+++ b/Test/aitest1/Linear8.bpl
@@ -0,0 +1,42 @@
+
+procedure foo () returns ()
+{
+  var i: int;
+  var j: int;
+  var n: int;
+
+A:  // true
+  n := 0;
+  goto B;
+
+B:  // n = 0
+  j := 0;
+  goto C;
+
+C:  // n = 0 AND j = 0
+  i := j + 1;
+  goto D;
+
+D:  // n = 0 AND j = 0 AND i = j + 1
+  i := i + 1;
+  goto E;
+
+E:  // n = 0 AND j = 0 AND i = j + 2
+  i := i + 1;
+  goto F;
+
+F:  // n = 0 AND j = 0 AND i = j + 3
+  i := i + 1;
+  goto G;
+
+G:  // n = 0 AND j = 0 AND i = j + 4
+  i := i + 1;
+  goto H;
+
+H:  // n = 0 AND j = 0 AND i = j + 1
+  j := j + 1;
+  goto I;
+
+I:  // n = 0 AND j = 1 AND i = j + 4
+  return;
+}
diff --git a/Test/aitest1/Linear9.bpl b/Test/aitest1/Linear9.bpl
new file mode 100644
index 00000000..e48a7a0c
--- /dev/null
+++ b/Test/aitest1/Linear9.bpl
@@ -0,0 +1,29 @@
+procedure foo () returns ()
+{
+  var i: int;
+  var j: int;
+  var n: int;
+entry:
+  assume n >= 4;
+  i := 0;
+  j := i + 1;
+  // n >= 4 AND i = 0 AND j = i+1
+  goto exit, loop0;
+
+loop0:
+  // n >= 4 AND i >= 0 AND j = i+1
+  assume j <= n;
+  goto loop1;
+loop1:
+  // n >= 4 AND i >= 0 AND j = i+1 AND j <= n
+  i := i + 1;
+  goto loop2;
+loop2:
+  j := j + 1;
+  // n >= 4 AND i >= 1 AND j = i+1 AND j <= n+1
+  goto loop0, exit;
+
+exit:
+  // n >= 4 AND i >= 0 AND j = i+1 AND j <= n+1
+  return;
+}
diff --git a/Test/aitest1/Output b/Test/aitest1/Output
new file mode 100644
index 00000000..4e5c8f27
--- /dev/null
+++ b/Test/aitest1/Output
@@ -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
diff --git a/Test/aitest1/ineq.bpl b/Test/aitest1/ineq.bpl
new file mode 100644
index 00000000..a417aaf3
--- /dev/null
+++ b/Test/aitest1/ineq.bpl
@@ -0,0 +1,81 @@
+// Test the polyhedra domain for linear inequalities
+
+
+procedure SimpleLoop ()
+{  
+  var i : int;
+  
+  start:
+    i := 0;
+    goto test;
+ 
+  test:
+    goto Then, Else;
+
+  Then:
+    assume i < 10;
+    i := i + 1;
+    goto test;
+
+  Else:
+    assume ! (i < 10);
+    return;
+}    
+
+
+procedure VariableBoundLoop (n : int)
+{  
+  var i : int;
+  
+  start:
+    i := 0;
+    goto test;
+ 
+  test:
+    goto Then, Else;
+
+  Then:
+    assume i < n;
+    i := i + 1;
+    goto test;
+
+  Else:
+    assume ! (i < n);
+    return;
+}    
+
+procedure Foo () 
+{
+ var i : int;
+
+ start:
+ i := 3 * i + 1;
+ i := 3 * (i + 1);
+ i := 1 + 3 * i;
+ i := (i + 1) * 3 ;
+ return;
+}
+
+procedure FooToo () 
+{
+ var i : int;
+
+ start:
+ i := 5;
+ i := 3 * i + 1;
+ i := 3 * (i + 1);
+ i := 1 + 3 * i;
+ i := (i + 1) * 3 ;
+ return;
+}
+
+procedure FooTooStepByStep () 
+{
+ var i : int;
+
+ L0: i := 5; goto L1;
+ L1: i := 3 * i + 1; goto L2;
+ L2: i := 3 * (i + 1); goto L3;
+ L3: i := 1 + 3 * i; goto L4;
+ L4: i := (i + 1) * 3; return;
+}
diff --git a/Test/aitest1/runtest.bat b/Test/aitest1/runtest.bat
new file mode 100644
index 00000000..f2a4d3e5
--- /dev/null
+++ b/Test/aitest1/runtest.bat
@@ -0,0 +1,17 @@
+@echo off
+setlocal
+
+set BGEXE=..\..\Binaries\Boogie.exe
+
+for %%f in (ineq.bpl Linear0.bpl Linear1.bpl Linear2.bpl
+     Linear3.bpl Linear4.bpl Linear5.bpl Linear6.bpl
+     Linear7.bpl Linear8.bpl Linear9.bpl) do (
+  echo -------------------- %%f --------------------
+  %BGEXE% %* -infer:p -printInstrumented -noVerify %%f
+)
+
+for %%f in (Bound.bpl) do (
+  echo -------------------- %%f -------------------- 
+  %BGEXE% %* -infer:p %%f
+)
+
author	mikebarnett <unknown>	2009-07-15 21:03:41 +0000
committer	mikebarnett <unknown>	2009-07-15 21:03:41 +0000
commit	ce1c2de044c91624370411e23acab13b0381949b (patch)
tree	592539996fe08050ead5ee210c973801611dde40 /Test/aitest1