From 95a42a224dff8eae383d93beb37a3da6a28bb0f3 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Fri, 28 Aug 2015 20:50:50 -0700
Subject: Suppress many warnings in the test suite.

We already have separate tests for those, and we want the output to be the same
with and without /autoTriggers.
---
 Test/dafny1/PriorityQueue.dfy | 32 ++++++++++++++++----------------
 1 file changed, 16 insertions(+), 16 deletions(-)

(limited to 'Test/dafny1/PriorityQueue.dfy')

diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index 94223cba..3d2a5d78 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -12,7 +12,7 @@ class PriorityQueue {
     reads this, Repr;
   {
     MostlyValid() &&
-    (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])
+    (forall j {:nowarn} :: 2 <= j && j <= n ==> a[j/2] <= a[j])
   }
 
   predicate MostlyValid()
@@ -50,8 +50,8 @@ class PriorityQueue {
   method SiftUp(k: int)
     requires 1 <= k && k <= n;
     requires MostlyValid();
-    requires (forall j :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);
-    requires (forall j :: 1 <= j && j <= n ==> j/2 != k);  // k is a leaf
+    requires (forall j {:nowarn} :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);
+    requires (forall j {:nowarn} :: 1 <= j && j <= n ==> j/2 != k);  // k is a leaf
     modifies a;
     ensures Valid();
   {
@@ -59,8 +59,8 @@ class PriorityQueue {
     assert MostlyValid();
     while (1 < i)
       invariant i <= k && MostlyValid();
-      invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
-      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
+      invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
     {
       if (a[i/2] <= a[i]) {
         return;
@@ -85,8 +85,8 @@ class PriorityQueue {
   method SiftDown(k: int)
     requires 1 <= k;
     requires MostlyValid();
-    requires (forall j :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);
-    requires (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);
+    requires (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);
+    requires (forall j {:nowarn} :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);
     // Alternatively, the line above can be expressed as:
     //     requires (forall j :: 1 <= k/2 && j/2 == k && j <= n ==> a[j/2/2] <= a[j]);
     modifies a;
@@ -95,8 +95,8 @@ class PriorityQueue {
     var i := k;
     while (2*i <= n)  // while i is not a leaf
       invariant 1 <= i && MostlyValid();
-      invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
-      invariant (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);
+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);
     {
       var smallestChild;
       if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {
@@ -127,7 +127,7 @@ class PriorityQueue_Alternative {
     reads this, Repr;
   {
     MostlyValid() &&
-    (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])
+    (forall j {:nowarn} :: 2 <= j && j <= n ==> a[j/2] <= a[j])
   }
 
   predicate MostlyValid()
@@ -164,7 +164,7 @@ class PriorityQueue_Alternative {
 
   method SiftUp()
     requires MostlyValid();
-    requires (forall j :: 2 <= j && j <= n && j != n ==> a[j/2] <= a[j]);
+    requires (forall j {:nowarn} :: 2 <= j && j <= n && j != n ==> a[j/2] <= a[j]);
     modifies a;
     ensures Valid();
   {
@@ -172,8 +172,8 @@ class PriorityQueue_Alternative {
     assert MostlyValid();
     while (1 < i)
       invariant i <= n && MostlyValid();
-      invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
-      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
+      invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
     {
       if (a[i/2] <= a[i]) {
         return;
@@ -197,15 +197,15 @@ class PriorityQueue_Alternative {
 
   method SiftDown()
     requires MostlyValid();
-    requires (forall j :: 4 <= j && j <= n ==> a[j/2] <= a[j]);
+    requires (forall j {:nowarn} :: 4 <= j && j <= n ==> a[j/2] <= a[j]);
     modifies a;
     ensures Valid();
   {
     var i := 1;
     while (2*i <= n)  // while i is not a leaf
       invariant 1 <= i && MostlyValid();
-      invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
-      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
+      invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
     {
       var smallestChild;
       if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {
-- 
cgit v1.2.3