From de994ac942cd6a017f2f277bd0be37a7e8cc0c98 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Mon, 12 Dec 2011 13:53:32 -0800
Subject: Dafny: implemented thresholds for the new interval domain (/infer:j)

---
 Test/aitest0/Answer        | 14 ++++++++++--
 Test/aitest0/Intervals.bpl | 56 ++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 68 insertions(+), 2 deletions(-)

(limited to 'Test/aitest0')

diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
index e517aa18..73a9509c 100644
--- a/Test/aitest0/Answer
+++ b/Test/aitest0/Answer
@@ -109,5 +109,15 @@ implementation Evaluate()
 
 
 Boogie program verifier finished with 0 verified, 0 errors
-
-Boogie program verifier finished with 1 verified, 0 errors
+Intervals.bpl(62,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    Intervals.bpl(57,5): anon0
+    Intervals.bpl(58,3): anon3_LoopHead
+    Intervals.bpl(58,3): anon3_LoopDone
+Intervals.bpl(73,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    Intervals.bpl(68,5): anon0
+    Intervals.bpl(69,3): anon3_LoopHead
+    Intervals.bpl(69,3): anon3_LoopDone
+
+Boogie program verifier finished with 4 verified, 2 errors
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
index 49d27b1c..7ed2c3d2 100644
--- a/Test/aitest0/Intervals.bpl
+++ b/Test/aitest0/Intervals.bpl
@@ -17,3 +17,59 @@ procedure P(K: int)
   }
   assert 13 <= x;
 }
+
+procedure Thresholds0()
+{
+  var i: int;
+  i := 0;
+  while (i < 200)
+  {
+    i := i + 1;
+  }
+  assert i == 200;
+}
+
+procedure Thresholds1()
+{
+  var i: int;
+  i := 0;
+  while (i <= 199)
+  {
+    i := i + 1;
+  }
+  assert i == 200;
+}
+
+procedure Thresholds2()
+{
+  var i: int;
+  i := 100;
+  while (0 < i)
+  {
+    i := i - 1;
+  }
+  assert i == 0;
+}
+
+procedure Thresholds3()
+{
+  var i: int;
+  i := 0;
+  while (i < 200)
+  {
+    i := i + 1;
+  }
+  assert i == 199;  // error
+}
+
+procedure Thresholds4()
+{
+  var i: int;
+  i := 0;
+  while (i + 3 < 203)
+  {
+    i := i + 1;
+  }
+  assert i * 2 == 400;  // error: this would hold in an execution, but /infer:j is too weak to infer invariant i<=200
+}
+
-- 
cgit v1.2.3