diff options
author | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-28 20:50:50 -0700 |
---|---|---|
committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-28 20:50:50 -0700 |
commit | 95a42a224dff8eae383d93beb37a3da6a28bb0f3 (patch) | |
tree | 9a3b1f5fcba891aa5878a27528fa4ca619b8af6a /Test/dafny4 | |
parent | 3d45aa05a023c092167d938a72adf78cf1f76fdf (diff) |
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.
Diffstat (limited to 'Test/dafny4')
-rw-r--r-- | Test/dafny4/Bug60.dfy | 4 | ||||
-rw-r--r-- | Test/dafny4/Bug63.dfy | 4 | ||||
-rw-r--r-- | Test/dafny4/Primes.dfy | 8 |
3 files changed, 8 insertions, 8 deletions
diff --git a/Test/dafny4/Bug60.dfy b/Test/dafny4/Bug60.dfy index 5340ad6b..c433451c 100644 --- a/Test/dafny4/Bug60.dfy +++ b/Test/dafny4/Bug60.dfy @@ -9,5 +9,5 @@ method Main() print (s, m), "\n";
print (|s|, |m|), "\n";
print(set s | s in m), "\n";
- print (forall x :: x in (map [1:=10, 2:=20]) ==> x > 0), "\n";
-}
\ No newline at end of file + print (forall x {:nowarn} :: x in (map [1:=10, 2:=20]) ==> x > 0), "\n";
+}
diff --git a/Test/dafny4/Bug63.dfy b/Test/dafny4/Bug63.dfy index 86aad232..39cbae1b 100644 --- a/Test/dafny4/Bug63.dfy +++ b/Test/dafny4/Bug63.dfy @@ -8,6 +8,6 @@ method M() method Client()
{
- assume forall o: object :: o != null ==> false;
+ assume forall o: object {:nowarn} :: o != null ==> false;
M();
-}
\ No newline at end of file +}
diff --git a/Test/dafny4/Primes.dfy b/Test/dafny4/Primes.dfy index b0bb7527..fd64b45e 100644 --- a/Test/dafny4/Primes.dfy +++ b/Test/dafny4/Primes.dfy @@ -3,7 +3,7 @@ predicate IsPrime(n: int)
{
- 2 <= n && forall m :: 2 <= m < n ==> n % m != 0
+ 2 <= n && forall m {:nowarn} :: 2 <= m < n ==> n % m != 0 // WISH It would be great to think about the status of modulo as a trigger
}
// The following theorem shows that there is an infinite number of primes
@@ -167,8 +167,8 @@ lemma Composite(c: int) returns (a: int, b: int) calc {
true;
!IsPrime(c);
- !(2 <= c && forall m :: 2 <= m < c ==> c % m != 0);
- exists m :: 2 <= m < c && c % m == 0;
+ !(2 <= c && forall m {:nowarn} :: 2 <= m < c ==> c % m != 0);
+ exists m {:nowarn} :: 2 <= m < c && c % m == 0;
}
a :| 2 <= a < c && c % a == 0;
b := c / a;
@@ -194,7 +194,7 @@ lemma LargestElementExists(s: set<int>) var s' := s;
while true
invariant s' != {} && s' <= s;
- invariant forall x,y :: x in s' && y in s - s' ==> y <= x;
+ invariant forall x,y {:nowarn} :: x in s' && y in s - s' ==> y <= x;
decreases s';
{
var x :| x in s'; // pick something
|