Boogie: Added new abstract interpretation harness, which uses native Boogie Expr's, not the more abstract AIExpr's.

Boogie: Added Trivial Domain (/infer:t), which just detects assume/assert false.
Boogie: Added new Interval Domain (/infer:j), which is stronger than the /infer:i intervals (because the also include preconditions, booleans, and more constraints) and may also be more efficient than previous intervals
Boogie: Mark all inferred conditions with attribute {:inferred}

3 files changed, 40 insertions, 18 deletions

diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
index 58750460..e517aa18 100644
--- a/Test/aitest0/Answer
+++ b/Test/aitest0/Answer
@@ -18,34 +18,34 @@ implementation Join(b: bool)
   var z: int;

 

   start:

-    assume true;

+    assume {:inferred} true;

     GlobalFlag := true;

     x := 3;

     y := 4;

     z := x + y;

-    assume x == 3 && y == 4 && z == 7;

+    assume {:inferred} x == 3 && y == 4 && z == 7;

     goto Then, Else;

 

   Then:

-    assume x == 3 && y == 4 && z == 7;

+    assume {:inferred} x == 3 && y == 4 && z == 7;

     assume b <==> true;

     x := x + 1;

-    assume x == 4 && y == 4 && z == 7;

+    assume {:inferred} x == 4 && y == 4 && z == 7;

     goto join;

 

   Else:

-    assume x == 3 && y == 4 && z == 7;

+    assume {:inferred} x == 3 && y == 4 && z == 7;

     assume b <==> false;

     y := 4;

-    assume x == 3 && y == 4 && z == 7;

+    assume {:inferred} x == 3 && y == 4 && z == 7;

     goto join;

 

   join:

-    assume y == 4 && z == 7;

+    assume {:inferred} y == 4 && z == 7;

     assert y == 4;

     assert z == 7;

     assert GlobalFlag <==> true;

-    assume y == 4 && z == 7;

+    assume {:inferred} y == 4 && z == 7;

     return;

 }

 

@@ -61,27 +61,27 @@ implementation Loop()
   var i: int;

 

   start:

-    assume true;

+    assume {:inferred} true;

     c := 0;

     i := 0;

-    assume c == 0 && i == 0;

+    assume {:inferred} c == 0 && i == 0;

     goto test;

 

   test:  // cut point

-    assume c == 0;

-    assume c == 0;

+    assume {:inferred} c == 0;

+    assume {:inferred} c == 0;

     goto Then, Else;

 

   Then:

-    assume c == 0;

+    assume {:inferred} c == 0;

     assume i < 10;

     i := i + 1;

-    assume c == 0;

+    assume {:inferred} c == 0;

     goto test;

 

   Else:

-    assume c == 0;

-    assume c == 0;

+    assume {:inferred} c == 0;

+    assume {:inferred} c == 0;

     return;

 }

 

@@ -96,16 +96,18 @@ implementation Evaluate()
   var i: int;

 

   start:

-    assume true;

+    assume {:inferred} true;

     i := 5;

     i := 3 * i + 1;

     i := 3 * (i + 1);

     i := 1 + 3 * i;

     i := (i + 1) * 3;

-    assume i == 465;

+    assume {:inferred} i == 465;

     return;

 }

 

 

 

 Boogie program verifier finished with 0 verified, 0 errors

+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
new file mode 100644
index 00000000..49d27b1c
--- /dev/null
+++ b/Test/aitest0/Intervals.bpl
@@ -0,0 +1,19 @@
+const N: int;

+axiom 0 <= N;

+

+procedure P(K: int)

+  requires 0 <= K;

+{

+  var b: bool, x, k: int;

+

+  if (!b) {

+    b := !b;

+  }

+  x := if b then 13 else 10;

+  k := K;

+  while (k != 0) {

+    x := x + k;

+    k := k - 1;

+  }

+  assert 13 <= x;

+}

diff --git a/Test/aitest0/runtest.bat b/Test/aitest0/runtest.bat
index a4c12d8d..1cb7a60c 100644
--- a/Test/aitest0/runtest.bat
+++ b/Test/aitest0/runtest.bat
@@ -4,3 +4,4 @@ setlocal
 set BGEXE=..\..\Binaries\Boogie.exe

 

 %BGEXE% %* -infer:c -instrumentInfer:e -printInstrumented -noVerify constants.bpl

+%BGEXE% %* -infer:j Intervals.bpl