From 95bb8b3b4454fdc1a14fd67b22a5ac6183135cfd Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Mon, 5 Dec 2011 23:07:06 -0800
Subject: 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}

---
 Test/aitest1/Answer | 140 ++++++++++++++++++++++++++--------------------------
 1 file changed, 70 insertions(+), 70 deletions(-)

(limited to 'Test/aitest1')

diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer
index ca9ff22a..718e7171 100644
--- a/Test/aitest1/Answer
+++ b/Test/aitest1/Answer
@@ -8,27 +8,27 @@ implementation SimpleLoop()
   var i: int;
 
   start:
-    assume true;
+    assume {:inferred} true;
     i := 0;
-    assume i == 0;
+    assume {:inferred} i == 0;
     goto test;
 
   test:  // cut point
-    assume 0 <= i;
-    assume 0 <= i;
+    assume {:inferred} 0 <= i;
+    assume {:inferred} 0 <= i;
     goto Then, Else;
 
   Then:
-    assume 0 <= i;
+    assume {:inferred} 0 <= i;
     assume i < 10;
     i := i + 1;
-    assume i <= 10 && 1 <= i;
+    assume {:inferred} i <= 10 && 1 <= i;
     goto test;
 
   Else:
-    assume 0 <= i;
+    assume {:inferred} 0 <= i;
     assume !(i < 10);
-    assume 10 <= i;
+    assume {:inferred} 10 <= i;
     return;
 }
 
@@ -43,27 +43,27 @@ implementation VariableBoundLoop(n: int)
   var i: int;
 
   start:
-    assume true;
+    assume {:inferred} true;
     i := 0;
-    assume i == 0;
+    assume {:inferred} i == 0;
     goto test;
 
   test:  // cut point
-    assume 0 <= i;
-    assume 0 <= i;
+    assume {:inferred} 0 <= i;
+    assume {:inferred} 0 <= i;
     goto Then, Else;
 
   Then:
-    assume 0 <= i;
+    assume {:inferred} 0 <= i;
     assume i < n;
     i := i + 1;
-    assume i <= n && 1 <= i;
+    assume {:inferred} i <= n && 1 <= i;
     goto test;
 
   Else:
-    assume 0 <= i;
+    assume {:inferred} 0 <= i;
     assume !(i < n);
-    assume n <= i && 0 <= i;
+    assume {:inferred} n <= i && 0 <= i;
     return;
 }
 
@@ -78,12 +78,12 @@ implementation Foo()
   var i: int;
 
   start:
-    assume true;
+    assume {:inferred} true;
     i := 3 * i + 1;
     i := 3 * (i + 1);
     i := 1 + 3 * i;
     i := (i + 1) * 3;
-    assume true;
+    assume {:inferred} true;
     return;
 }
 
@@ -98,13 +98,13 @@ implementation FooToo()
   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 1 / 3 * i == 155;
+    assume {:inferred} 1 / 3 * i == 155;
     return;
 }
 
@@ -119,13 +119,13 @@ implementation FooTooStepByStep()
   var i: int;
 
   L0:
-    assume true;
+    assume {:inferred} true;
     i := 5;
     i := 3 * i + 1;
     i := 3 * (i + 1);
     i := 1 + 3 * i;
     i := (i + 1) * 3;
-    assume 1 / 3 * i == 155;
+    assume {:inferred} 1 / 3 * i == 155;
     return;
 }
 
@@ -145,8 +145,8 @@ implementation p()
 {
 
   start:
-    assume true;
-    assume true;
+    assume {:inferred} true;
+    assume {:inferred} true;
     return;
 }
 
@@ -166,9 +166,9 @@ implementation p()
 {
 
   start:
-    assume true;
+    assume {:inferred} true;
     assume x * x == y;
-    assume true;
+    assume {:inferred} true;
     return;
 }
 
@@ -188,9 +188,9 @@ implementation p()
 {
 
   start:
-    assume true;
-    assume x == 8;
+    assume {:inferred} true;
     assume x == 8;
+    assume {:inferred} x == 8;
     return;
 }
 
@@ -210,9 +210,9 @@ implementation p()
 {
 
   start:
-    assume true;
+    assume {:inferred} true;
     assume x < y;
-    assume x + 1 <= y;
+    assume {:inferred} x + 1 <= y;
     return;
 }
 
@@ -233,20 +233,20 @@ implementation p()
 {
 
   A:
-    assume true;
+    assume {:inferred} true;
     assume x < y;
-    assume x + 1 <= y;
+    assume {:inferred} x + 1 <= y;
     goto B, C;
 
   B:
-    assume x + 1 <= y;
+    assume {:inferred} x + 1 <= y;
     x := x * x;
-    assume true;
+    assume {:inferred} true;
     return;
 
   C:
-    assume x + 1 <= y;
-    assume x + 1 <= y;
+    assume {:inferred} x + 1 <= y;
+    assume {:inferred} x + 1 <= y;
     return;
 }
 
@@ -267,32 +267,32 @@ implementation p()
 {
 
   A:
-    assume true;
+    assume {:inferred} true;
     assume 0 - 1 <= x;
-    assume -1 <= x;
+    assume {:inferred} -1 <= x;
     goto B, E;
 
   B:
-    assume -1 <= x;
+    assume {:inferred} -1 <= x;
     assume x < y;
-    assume x + 1 <= y && -1 <= x;
+    assume {:inferred} x + 1 <= y && -1 <= x;
     goto C, E;
 
   C:
-    assume x + 1 <= y && -1 <= x;
+    assume {:inferred} x + 1 <= y && -1 <= x;
     x := x * x;
-    assume 0 <= y;
+    assume {:inferred} 0 <= y;
     goto D, E;
 
   D:
-    assume 0 <= y;
+    assume {:inferred} 0 <= y;
     x := y;
-    assume x == y && 0 <= y;
+    assume {:inferred} x == y && 0 <= y;
     return;
 
   E:
-    assume true;
-    assume true;
+    assume {:inferred} true;
+    assume {:inferred} true;
     return;
 }
 
@@ -315,26 +315,26 @@ implementation p()
 {
 
   A:
-    assume true;
+    assume {:inferred} true;
     x := 8;
-    assume x == 8;
+    assume {:inferred} x == 8;
     goto B, C;
 
   B:
-    assume x == 8;
+    assume {:inferred} x == 8;
     x := 9;
-    assume x == 9;
+    assume {:inferred} x == 9;
     goto D;
 
   C:
-    assume x == 8;
+    assume {:inferred} x == 8;
     x := 10;
-    assume x == 10;
+    assume {:inferred} x == 10;
     goto D;
 
   D:
-    assume 9 <= x && x <= 10;
-    assume 9 <= x && x <= 10;
+    assume {:inferred} 9 <= x && x <= 10;
+    assume {:inferred} 9 <= x && x <= 10;
     return;
 }
 
@@ -356,25 +356,25 @@ implementation p()
 {
 
   A:
-    assume true;
-    assume true;
+    assume {:inferred} true;
+    assume {:inferred} true;
     goto B, C;
 
   B:
-    assume true;
-    assume x <= 0;
+    assume {:inferred} true;
     assume x <= 0;
+    assume {:inferred} x <= 0;
     goto D;
 
   C:
-    assume true;
-    assume y <= 0;
+    assume {:inferred} true;
     assume y <= 0;
+    assume {:inferred} y <= 0;
     goto D;
 
   D:
-    assume true;
-    assume true;
+    assume {:inferred} true;
+    assume {:inferred} true;
     return;
 }
 
@@ -393,7 +393,7 @@ implementation foo()
   var n: int;
 
   A:
-    assume true;
+    assume {:inferred} true;
     n := 0;
     j := 0;
     i := j + 1;
@@ -402,7 +402,7 @@ implementation foo()
     i := i + 1;
     i := i + 1;
     j := j + 1;
-    assume i == j + 4 && j == 1 && n == 0;
+    assume {:inferred} i == j + 4 && j == 1 && n == 0;
     return;
 }
 
@@ -421,24 +421,24 @@ implementation foo()
   var n: int;
 
   entry:
-    assume true;
+    assume {:inferred} true;
     assume n >= 4;
     i := 0;
     j := i + 1;
-    assume j == i + 1 && i == 0 && 4 <= n;
+    assume {:inferred} j == i + 1 && i == 0 && 4 <= n;
     goto exit, loop0;
 
   loop0:  // cut point
-    assume 4 <= n && 0 <= i && j == i + 1;
+    assume {:inferred} 4 <= n && 0 <= i && j == i + 1;
     assume j <= n;
     i := i + 1;
     j := j + 1;
-    assume j <= n + 1 && j == i + 1 && 1 <= i && 4 <= n;
+    assume {:inferred} j <= n + 1 && j == i + 1 && 1 <= i && 4 <= n;
     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;
+    assume {:inferred} j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;
+    assume {:inferred} j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;
     return;
 }
 
-- 
cgit v1.2.3