Enable Linear inequality lit tests.

25 files changed, 472 insertions, 5 deletions

diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer
index 880e587b..f5b5de90 100644
--- a/Test/aitest1/Answer
+++ b/Test/aitest1/Answer
@@ -446,10 +446,10 @@ implementation foo()
 

 Boogie program verifier finished with 0 verified, 0 errors

 -------------------- Bound.bpl -------------------- 

-Bound.bpl(24,3): Error BP5001: This assertion might not hold.

+Bound.bpl(26,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    Bound.bpl(8,1): start

-    Bound.bpl(14,1): LoopHead

-    Bound.bpl(22,1): AfterLoop

+    Bound.bpl(10,1): start

+    Bound.bpl(16,1): LoopHead

+    Bound.bpl(24,1): AfterLoop

 

 Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/aitest1/Bound.bpl b/Test/aitest1/Bound.bpl
index 02b2c460..7df27414 100644
--- a/Test/aitest1/Bound.bpl
+++ b/Test/aitest1/Bound.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -infer:j %s > %t

+// RUN: %diff %s.expect %t

 const TEST: name;

 

 procedure P()

@@ -25,4 +27,4 @@ AfterLoop:
   return;

 }

 

-type name;
\ No newline at end of file
+type name;

diff --git a/Test/aitest1/Bound.bpl.expect b/Test/aitest1/Bound.bpl.expect
new file mode 100644
index 00000000..46c18d30
--- /dev/null
+++ b/Test/aitest1/Bound.bpl.expect
@@ -0,0 +1,7 @@
+Bound.bpl(26,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    Bound.bpl(10,1): start
+    Bound.bpl(16,1): LoopHead
+    Bound.bpl(24,1): AfterLoop
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/aitest1/Linear0.bpl b/Test/aitest1/Linear0.bpl
index 7a11c803..3a74b1e9 100644
--- a/Test/aitest1/Linear0.bpl
+++ b/Test/aitest1/Linear0.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t

+// RUN: %diff %s.expect %t

 // Simple test file for checking the inference of linear constraints.

 

 var x: int;

diff --git a/Test/aitest1/Linear0.bpl.expect b/Test/aitest1/Linear0.bpl.expect
new file mode 100644
index 00000000..5950e8d1
--- /dev/null
+++ b/Test/aitest1/Linear0.bpl.expect
@@ -0,0 +1,20 @@
+var x: int;
+
+var y: int;
+
+procedure p();
+
+
+
+implementation p()
+{
+
+  start:
+    assume {:inferred} true;
+    assume {:inferred} true;
+    return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/aitest1/Linear1.bpl b/Test/aitest1/Linear1.bpl
index 0cbb4a07..505d1a11 100644
--- a/Test/aitest1/Linear1.bpl
+++ b/Test/aitest1/Linear1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t

+// RUN: %diff %s.expect %t

 // Simple test file for checking the inference of linear constraints.

 

 var x: int;

diff --git a/Test/aitest1/Linear1.bpl.expect b/Test/aitest1/Linear1.bpl.expect
new file mode 100644
index 00000000..5e2c8d04
--- /dev/null
+++ b/Test/aitest1/Linear1.bpl.expect
@@ -0,0 +1,21 @@
+var x: int;
+
+var y: int;
+
+procedure p();
+
+
+
+implementation p()
+{
+
+  start:
+    assume {:inferred} true;
+    assume x * x == y;
+    assume {:inferred} true;
+    return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/aitest1/Linear2.bpl b/Test/aitest1/Linear2.bpl
index 9e02c9e2..de1da8a1 100644
--- a/Test/aitest1/Linear2.bpl
+++ b/Test/aitest1/Linear2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t

+// RUN: %diff %s.expect %t

 // Simple test file for checking the inference of linear constraints.

 

 var x: int;

diff --git a/Test/aitest1/Linear2.bpl.expect b/Test/aitest1/Linear2.bpl.expect
new file mode 100644
index 00000000..6d8b9403
--- /dev/null
+++ b/Test/aitest1/Linear2.bpl.expect
@@ -0,0 +1,21 @@
+var x: int;
+
+var y: int;
+
+procedure p();
+
+
+
+implementation p()
+{
+
+  start:
+    assume {:inferred} true;
+    assume x == 8;
+    assume {:inferred} x == 8;
+    return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/aitest1/Linear3.bpl b/Test/aitest1/Linear3.bpl
index c6b7a441..4b91bd0f 100644
--- a/Test/aitest1/Linear3.bpl
+++ b/Test/aitest1/Linear3.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t

+// RUN: %diff %s.expect %t

 // Simple test file for checking the inference of linear constraints.

 

 var x: int;

diff --git a/Test/aitest1/Linear3.bpl.expect b/Test/aitest1/Linear3.bpl.expect
new file mode 100644
index 00000000..e65b3971
--- /dev/null
+++ b/Test/aitest1/Linear3.bpl.expect
@@ -0,0 +1,21 @@
+var x: int;
+
+var y: int;
+
+procedure p();
+
+
+
+implementation p()
+{
+
+  start:
+    assume {:inferred} true;
+    assume x < y;
+    assume {:inferred} true;
+    return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/aitest1/Linear4.bpl b/Test/aitest1/Linear4.bpl
index 2207debe..c3e908f2 100644
--- a/Test/aitest1/Linear4.bpl
+++ b/Test/aitest1/Linear4.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t

+// RUN: %diff %s.expect %t

 // Simple test file for checking the inference of linear constraints.

 

 var x: int;

diff --git a/Test/aitest1/Linear4.bpl.expect b/Test/aitest1/Linear4.bpl.expect
new file mode 100644
index 00000000..29b3c226
--- /dev/null
+++ b/Test/aitest1/Linear4.bpl.expect
@@ -0,0 +1,33 @@
+var x: int;
+
+var y: int;
+
+procedure p();
+  modifies x;
+
+
+
+implementation p()
+{
+
+  A:
+    assume {:inferred} true;
+    assume x < y;
+    assume {:inferred} true;
+    goto B, C;
+
+  C:
+    assume {:inferred} true;
+    assume {:inferred} true;
+    return;
+
+  B:
+    assume {:inferred} true;
+    x := x * x;
+    assume {:inferred} true;
+    return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/aitest1/Linear5.bpl b/Test/aitest1/Linear5.bpl
index 199cb6f2..69cbb7a7 100644
--- a/Test/aitest1/Linear5.bpl
+++ b/Test/aitest1/Linear5.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t

+// RUN: %diff %s.expect %t

 // Simple test file for checking the inference of linear constraints.

 

 var x: int;

diff --git a/Test/aitest1/Linear5.bpl.expect b/Test/aitest1/Linear5.bpl.expect
new file mode 100644
index 00000000..fcd1ab08
--- /dev/null
+++ b/Test/aitest1/Linear5.bpl.expect
@@ -0,0 +1,45 @@
+var x: int;
+
+var y: int;
+
+procedure p();
+  modifies x;
+
+
+
+implementation p()
+{
+
+  A:
+    assume {:inferred} true;
+    assume -1 <= x;
+    assume {:inferred} -1 <= x;
+    goto B, E;
+
+  E:
+    assume {:inferred} true;
+    assume {:inferred} true;
+    return;
+
+  B:
+    assume {:inferred} -1 <= x;
+    assume x < y;
+    assume {:inferred} -1 <= x && 0 <= y;
+    goto C, E;
+
+  C:
+    assume {:inferred} -1 <= x && 0 <= y;
+    x := x * x;
+    assume {:inferred} x < 2 && 0 <= y;
+    goto D, E;
+
+  D:
+    assume {:inferred} x < 2 && 0 <= y;
+    x := y;
+    assume {:inferred} 0 <= x && 0 <= y;
+    return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/aitest1/Linear6.bpl b/Test/aitest1/Linear6.bpl
index 83e52a9a..7d066435 100644
--- a/Test/aitest1/Linear6.bpl
+++ b/Test/aitest1/Linear6.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t

+// RUN: %diff %s.expect %t

 // Simple test file for checking the inference of linear constraints.

 

 var x: int;

diff --git a/Test/aitest1/Linear6.bpl.expect b/Test/aitest1/Linear6.bpl.expect
new file mode 100644
index 00000000..1cb757b0
--- /dev/null
+++ b/Test/aitest1/Linear6.bpl.expect
@@ -0,0 +1,41 @@
+var x: int;
+
+var y: int;
+
+var z: int;
+
+procedure p();
+  modifies x;
+
+
+
+implementation p()
+{
+
+  A:
+    assume {:inferred} true;
+    x := 8;
+    assume {:inferred} x == 8;
+    goto B, C;
+
+  C:
+    assume {:inferred} x == 8;
+    x := 10;
+    assume {:inferred} x == 10;
+    goto D;
+
+  D:
+    assume {:inferred} 9 <= x && x < 11;
+    assume {:inferred} 9 <= x && x < 11;
+    return;
+
+  B:
+    assume {:inferred} x == 8;
+    x := 9;
+    assume {:inferred} x == 9;
+    goto D;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/aitest1/Linear7.bpl b/Test/aitest1/Linear7.bpl
index b1bcaaaf..45514a67 100644
--- a/Test/aitest1/Linear7.bpl
+++ b/Test/aitest1/Linear7.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t

+// RUN: %diff %s.expect %t

 // Simple test file for checking the inference of linear constraints.

 

 var x: int;

diff --git a/Test/aitest1/Linear7.bpl.expect b/Test/aitest1/Linear7.bpl.expect
new file mode 100644
index 00000000..513b97dd
--- /dev/null
+++ b/Test/aitest1/Linear7.bpl.expect
@@ -0,0 +1,39 @@
+var x: int;
+
+var y: int;
+
+var z: int;
+
+procedure p();
+
+
+
+implementation p()
+{
+
+  A:
+    assume {:inferred} true;
+    assume {:inferred} true;
+    goto B, C;
+
+  C:
+    assume {:inferred} true;
+    assume y <= 0;
+    assume {:inferred} y < 1;
+    goto D;
+
+  D:
+    assume {:inferred} true;
+    assume {:inferred} true;
+    return;
+
+  B:
+    assume {:inferred} true;
+    assume x <= 0;
+    assume {:inferred} x < 1;
+    goto D;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/aitest1/Linear8.bpl b/Test/aitest1/Linear8.bpl
index 4bc3f887..14f396ad 100644
--- a/Test/aitest1/Linear8.bpl
+++ b/Test/aitest1/Linear8.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t

+// RUN: %diff %s.expect %t

 

 procedure foo () returns ()

 {

diff --git a/Test/aitest1/Linear8.bpl.expect b/Test/aitest1/Linear8.bpl.expect
new file mode 100644
index 00000000..f93f5770
--- /dev/null
+++ b/Test/aitest1/Linear8.bpl.expect
@@ -0,0 +1,27 @@
+procedure foo();
+
+
+
+implementation foo()
+{
+  var i: int;
+  var j: int;
+  var n: int;
+
+  A:
+    assume {:inferred} true;
+    n := 0;
+    j := 0;
+    i := j + 1;
+    i := i + 1;
+    i := i + 1;
+    i := i + 1;
+    i := i + 1;
+    j := j + 1;
+    assume {:inferred} i == 5 && j == 1 && n == 0;
+    return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/aitest1/Linear9.bpl b/Test/aitest1/Linear9.bpl
index e48a7a0c..1352bfb0 100644
--- a/Test/aitest1/Linear9.bpl
+++ b/Test/aitest1/Linear9.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t

+// RUN: %diff %s.expect %t

 procedure foo () returns ()

 {

   var i: int;

diff --git a/Test/aitest1/Linear9.bpl.expect b/Test/aitest1/Linear9.bpl.expect
new file mode 100644
index 00000000..23ac1698
--- /dev/null
+++ b/Test/aitest1/Linear9.bpl.expect
@@ -0,0 +1,35 @@
+procedure foo();
+
+
+
+implementation foo()
+{
+  var i: int;
+  var j: int;
+  var n: int;
+
+  entry:
+    assume {:inferred} true;
+    assume n >= 4;
+    i := 0;
+    j := i + 1;
+    assume {:inferred} i == 0 && j == 1 && 4 <= n;
+    goto exit, loop0;
+
+  loop0:  // cut point
+    assume {:inferred} 0 <= i && 1 <= j && 4 <= n;
+    assume j <= n;
+    i := i + 1;
+    j := j + 1;
+    assume {:inferred} 1 <= i && 2 <= j && 4 <= n;
+    goto loop0, exit;
+
+  exit:
+    assume {:inferred} 0 <= i && 1 <= j && 4 <= n;
+    assume {:inferred} 0 <= i && 1 <= j && 4 <= n;
+    return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/aitest1/ineq.bpl b/Test/aitest1/ineq.bpl
index a417aaf3..030c435c 100644
--- a/Test/aitest1/ineq.bpl
+++ b/Test/aitest1/ineq.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t

+// RUN: %diff %s.expect %t

 // Test the polyhedra domain for linear inequalities

 

 

diff --git a/Test/aitest1/ineq.bpl.expect b/Test/aitest1/ineq.bpl.expect
new file mode 100644
index 00000000..d6c36bdd
--- /dev/null
+++ b/Test/aitest1/ineq.bpl.expect
@@ -0,0 +1,133 @@
+procedure SimpleLoop();
+
+
+
+implementation SimpleLoop()
+{
+  var i: int;
+
+  start:
+    assume {:inferred} true;
+    i := 0;
+    assume {:inferred} i == 0;
+    goto test;
+
+  test:  // cut point
+    assume {:inferred} 0 <= i && i < 11;
+    assume {:inferred} 0 <= i && i < 11;
+    goto Then, Else;
+
+  Else:
+    assume {:inferred} 0 <= i && i < 11;
+    assume !(i < 10);
+    assume {:inferred} 0 <= i && i < 11;
+    return;
+
+  Then:
+    assume {:inferred} 0 <= i && i < 11;
+    assume i < 10;
+    i := i + 1;
+    assume {:inferred} 1 <= i && i < 11;
+    goto test;
+}
+
+
+
+procedure VariableBoundLoop(n: int);
+
+
+
+implementation VariableBoundLoop(n: int)
+{
+  var i: int;
+
+  start:
+    assume {:inferred} true;
+    i := 0;
+    assume {:inferred} i == 0;
+    goto test;
+
+  test:  // cut point
+    assume {:inferred} 0 <= i;
+    assume {:inferred} 0 <= i;
+    goto Then, Else;
+
+  Else:
+    assume {:inferred} 0 <= i;
+    assume !(i < n);
+    assume {:inferred} 0 <= i;
+    return;
+
+  Then:
+    assume {:inferred} 0 <= i;
+    assume i < n;
+    i := i + 1;
+    assume {:inferred} 1 <= i && 1 <= n;
+    goto test;
+}
+
+
+
+procedure Foo();
+
+
+
+implementation Foo()
+{
+  var i: int;
+
+  start:
+    assume {:inferred} true;
+    i := 3 * i + 1;
+    i := 3 * (i + 1);
+    i := 1 + 3 * i;
+    i := (i + 1) * 3;
+    assume {:inferred} true;
+    return;
+}
+
+
+
+procedure FooToo();
+
+
+
+implementation FooToo()
+{
+  var i: int;
+
+  start:
+    assume {:inferred} true;
+    i := 5;
+    i := 3 * i + 1;
+    i := 3 * (i + 1);
+    i := 1 + 3 * i;
+    i := (i + 1) * 3;
+    assume {:inferred} i == 465;
+    return;
+}
+
+
+
+procedure FooTooStepByStep();
+
+
+
+implementation FooTooStepByStep()
+{
+  var i: int;
+
+  L0:
+    assume {:inferred} true;
+    i := 5;
+    i := 3 * i + 1;
+    i := 3 * (i + 1);
+    i := 1 + 3 * i;
+    i := (i + 1) * 3;
+    assume {:inferred} i == 465;
+    return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors