diff options
Diffstat (limited to 'Test')
28 files changed, 145 insertions, 136 deletions
diff --git a/Test/dafny0/Comprehensions.dfy b/Test/dafny0/Comprehensions.dfy index d0436815..dd83e46c 100644 --- a/Test/dafny0/Comprehensions.dfy +++ b/Test/dafny0/Comprehensions.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
method M()
@@ -19,18 +19,18 @@ datatype D = A | B // have to run the resulting program to check that the compiler is doing the right thing.
method Main()
{
- var q := set i,j | 0 <= i && i < 10 && 0 <= j && j < 3 :: i+j;
+ var q := set i,j | 0 <= i < 10 && 0 <= j < 3 :: i+j;
PrintSet(q);
q := set b: bool | true :: if b then 3 else 7;
var d := set b:D | true;
- var test := forall d:D :: d == A || d == B;
+ var test := forall d:D {:nowarn} :: d == A || d == B; // Ignoring the warning as we're only compiling here
PrintSet(q);
var m := set k | k in q :: 2*k;
PrintSet(m);
PrintSet(set k | k in q && k % 2 == 0);
var sq := [30, 40, 20];
- PrintSet(set k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i);
- var bb := forall k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i == 17;
+ PrintSet(set k, i | k in sq && 0 <= i < k && i % 7 == 0 :: k + i);
+ var bb := forall k, i {:nowarn} | k in sq && 0 <= i < k && i % 7 == 0 :: k + i == 17; // Ignoring the warning as we're only compiling here
}
method PrintSet<T>(s: set<T>) {
diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy index c8c893a0..9e36e64c 100644 --- a/Test/dafny0/DTypes.dfy +++ b/Test/dafny0/DTypes.dfy @@ -5,7 +5,7 @@ class C { var n: set<Node>;
method M(v: Stack)
- requires v != null;
+ requires v != null
{
var o: object := v;
assert o !in n; // should be known from the types involved
@@ -28,12 +28,12 @@ class C { method A1(a: CP<int,C>)
{
var x: object := a;
- assert (forall b: CP<int,Stack> :: x == b ==> b == null); // follows from type antecedents
+ assert (forall b: CP<int,Stack> {:nowarn} :: x == b ==> b == null); // follows from type antecedents
}
var a2x: set<CP<C,Node>>;
method A2(b: set<CP<Node,C>>)
- requires null !in b;
+ requires null !in b
{
var x: set<object> := a2x;
var y: set<object> := b;
@@ -81,7 +81,7 @@ class CP<T,U> { datatype Data = Lemon | Kiwi(int)
function G(d: Data): int
- requires d != Data.Lemon;
+ requires d != Data.Lemon
{
match d
case Lemon => G(d)
@@ -101,28 +101,28 @@ class DatatypeInduction<T> { }
method Theorem0(tree: Tree<T>)
- ensures 1 <= LeafCount(tree);
+ ensures 1 <= LeafCount(tree)
{
assert (forall t: Tree<T> :: 1 <= LeafCount(t));
}
// also make sure it works for an instantiated generic datatype
method Theorem1(bt: Tree<bool>, it: Tree<int>)
- ensures 1 <= LeafCount(bt);
- ensures 1 <= LeafCount(it);
+ ensures 1 <= LeafCount(bt)
+ ensures 1 <= LeafCount(it)
{
assert (forall t: Tree<bool> :: 1 <= LeafCount(t));
assert (forall t: Tree<int> :: 1 <= LeafCount(t));
}
method NotATheorem0(tree: Tree<T>)
- ensures LeafCount(tree) % 2 == 1;
+ ensures LeafCount(tree) % 2 == 1
{
assert (forall t: Tree<T> :: LeafCount(t) % 2 == 1); // error: fails for Branch case
}
method NotATheorem1(tree: Tree<T>)
- ensures 2 <= LeafCount(tree);
+ ensures 2 <= LeafCount(tree)
{
assert (forall t: Tree<T> :: 2 <= LeafCount(t)); // error: fails for Leaf case
}
@@ -140,22 +140,22 @@ class DatatypeInduction<T> { // ----- here is a test for induction over integers
method IntegerInduction_Succeeds(a: array<int>)
- requires a != null;
- requires a.Length == 0 || a[0] == 0;
- requires forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1;
+ requires a != null
+ requires a.Length == 0 || a[0] == 0
+ requires forall j {:nowarn} :: 1 <= j < a.Length ==> a[j] == a[j-1]+2*j-1 // WISH: If induction was more powerful, we wouldn't need to rely on the quantifier to produce the j-1 term.
{
// The following assertion can be proved by induction:
- assert forall n {:induction} :: 0 <= n && n < a.Length ==> a[n] == n*n;
+ assert forall n {:induction} :: 0 <= n < a.Length ==> a[n] == n*n;
}
method IntegerInduction_Fails(a: array<int>)
- requires a != null;
- requires a.Length == 0 || a[0] == 0;
- requires forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1;
+ requires a != null
+ requires a.Length == 0 || a[0] == 0
+ requires forall j {:nowarn} :: 1 <= j < a.Length ==> a[j] == a[j-1]+2*j-1 // WISH: Same as above
{
// ...but the induction heuristics don't recognize the situation as one where
// applying induction would be profitable:
- assert forall n :: 0 <= n && n < a.Length ==> a[n] == n*n; // error reported
+ assert forall n :: 0 <= n < a.Length ==> a[n] == n*n; // error reported
}
}
@@ -171,7 +171,7 @@ abstract module OpaqueTypesWithParameters { }
method DifferentTypes(a: array<P<int>>, b: array<P<bool>>)
- requires a != null && b != null;
+ requires a != null && b != null
// If P were a known type, then it would also be known that P<int> and P<bool>
// would be different types, and then the types of 'a' and 'b' would be different,
// which would imply that the following postcondition would hold.
diff --git a/Test/dafny0/Matrix-OOB.dfy b/Test/dafny0/Matrix-OOB.dfy index 2e5c0366..d7aacd79 100644 --- a/Test/dafny0/Matrix-OOB.dfy +++ b/Test/dafny0/Matrix-OOB.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" /printTooltips "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// This is a regression test: OOB errors for matrices used to be reported on the
diff --git a/Test/dafny0/Matrix-OOB.dfy.expect b/Test/dafny0/Matrix-OOB.dfy.expect index 94e77aa4..e2920445 100644 --- a/Test/dafny0/Matrix-OOB.dfy.expect +++ b/Test/dafny0/Matrix-OOB.dfy.expect @@ -1,3 +1,4 @@ +Matrix-OOB.dfy(12,10): Info: Selected triggers: {m[i, j]}
Matrix-OOB.dfy(12,26): Error: index 0 out of range
Execution trace:
(0,0): anon0
@@ -6,6 +7,7 @@ Execution trace: (0,0): anon0
Matrix-OOB.dfy(13,0): Error BP5003: A postcondition might not hold on this return path.
Matrix-OOB.dfy(12,10): Related location: This is the postcondition that might not hold.
+Matrix-OOB.dfy(12,33): Related location
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy index 505d9b74..3ffa5a23 100644 --- a/Test/dafny0/Modules1.dfy +++ b/Test/dafny0/Modules1.dfy @@ -125,7 +125,7 @@ abstract module Regression { predicate p<c,d>(m: map<c,d>)
lemma m<a,b>(m: map<a,b>)
- ensures exists m :: p(var m : map<a,b> := m; m);
+ ensures exists m {:nowarn} :: p(var m : map<a,b> := m; m) // WISH: Zeta-expanding the let binding would provide a good trigger
}
abstract module B
diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy index e0d6491b..93a16475 100644 --- a/Test/dafny0/Parallel.dfy +++ b/Test/dafny0/Parallel.dfy @@ -210,7 +210,7 @@ class TwoState_C { ghost var data: int } // contexts are not allowed to allocate state. Callers of this ghost method will know
// that the postcondition is tantamount to 'false'.
ghost method TwoState0(y: int)
- ensures exists o: TwoState_C :: o != null && fresh(o)
+ ensures exists o: TwoState_C {:nowarn} :: o != null && fresh(o)
method TwoState_Main0() {
forall x { TwoState0(x); }
@@ -236,7 +236,7 @@ method X_Legit(c: TwoState_C) method TwoState_Main2()
{
forall x: int
- ensures exists o: TwoState_C :: o != null && fresh(o)
+ ensures exists o: TwoState_C {:nowarn} :: o != null && fresh(o)
{
TwoState0(x);
}
@@ -252,7 +252,7 @@ method TwoState_Main2() method TwoState_Main3()
{
forall x: int
- ensures exists o: TwoState_C :: o != null && fresh(o)
+ ensures exists o: TwoState_C {:nowarn} :: o != null && fresh(o)
{
assume false; // (there's no other way to achieve this forall-statement postcondition)
}
@@ -309,12 +309,12 @@ predicate ThProperty(step: nat, t: Nat, r: nat) {
match t
case Zero => true
- case Succ(o) => step>0 && exists ro:nat :: ThProperty(step-1, o, ro)
+ case Succ(o) => step>0 && exists ro:nat, ss | ss == step-1 :: ThProperty(ss, o, ro) //WISH: ss should be autogrnerated. Note that step is not a bound variable.
}
lemma Th(step: nat, t: Nat, r: nat)
requires t.Succ? && ThProperty(step, t, r)
// the next line follows from the precondition and the definition of ThProperty
- ensures exists ro:nat :: ThProperty(step-1, t.tail, ro)
+ ensures exists ro:nat, ss | ss == step-1 :: ThProperty(ss, t.tail, ro) //WISH same as above
{
}
diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy index 737dacd2..f8b3355d 100644 --- a/Test/dafny0/Predicates.dfy +++ b/Test/dafny0/Predicates.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
module A {
diff --git a/Test/dafny0/Predicates.dfy.expect b/Test/dafny0/Predicates.dfy.expect index 2d7ea6f1..36c9dfdd 100644 --- a/Test/dafny0/Predicates.dfy.expect +++ b/Test/dafny0/Predicates.dfy.expect @@ -17,10 +17,12 @@ Execution trace: (0,0): anon0
Predicates.dfy(164,4): Error BP5003: A postcondition might not hold on this return path.
Predicates.dfy(163,14): Related location: This is the postcondition that might not hold.
+Predicates.dfy(163,42): Related location
Execution trace:
(0,0): anon0
Predicates.dfy[Q1](154,4): Error BP5003: A postcondition might not hold on this return path.
Predicates.dfy[Q1](153,14): Related location: This is the postcondition that might not hold.
+Predicates.dfy[Q1](153,45): Related location
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/SeqFromArray.dfy b/Test/dafny0/SeqFromArray.dfy index 629c5045..cf889804 100644 --- a/Test/dafny0/SeqFromArray.dfy +++ b/Test/dafny0/SeqFromArray.dfy @@ -53,7 +53,7 @@ method L(a: array<int>, c: array<int>, n: nat) case A == C =>
assert forall i :: 0 <= i < h ==> A[i] == C[i];
case A == C =>
- assert forall i :: 0 <= i < h ==> a[n+i] == c[n+i];
+ assert forall i :: n <= i < n + h ==> a[i] == c[i];
case true =>
}
}
@@ -73,13 +73,13 @@ method M(a: array<int>, c: array<int>, m: nat, n: nat, k: nat, l: nat) } else if * {
assert forall i :: 0 <= i < n ==> A[i] == C[i];
} else if * {
- assert forall i :: k <= i < k+n ==> A[i-k] == C[i-k];
+ assert forall i {:nowarn} :: k <= i < k+n ==> A[i-k] == C[i-k];
} else if * {
assert forall i :: 0 <= i < n ==> A[i] == a[k+i];
} else if * {
assert forall i :: 0 <= i < n ==> C[i] == c[l+i];
} else if * {
- assert forall i :: 0 <= i < n ==> a[k+i] == c[l+i];
+ assert forall i {:nowarn} :: 0 <= i < n ==> a[k+i] == c[l+i];
}
}
case l+m <= c.Length && forall i :: 0 <= i < m ==> a[i] == c[l+i] =>
diff --git a/Test/dafny0/SeqFromArray.dfy.expect b/Test/dafny0/SeqFromArray.dfy.expect index 5395e298..af845d3e 100644 --- a/Test/dafny0/SeqFromArray.dfy.expect +++ b/Test/dafny0/SeqFromArray.dfy.expect @@ -1,6 +1,3 @@ -SeqFromArray.dfy(56,13): Warning: (!) No terms found to trigger on.
-SeqFromArray.dfy(76,17): Warning: (!) No terms found to trigger on.
-SeqFromArray.dfy(82,17): Warning: (!) No terms found to trigger on.
Dafny program verifier finished with 10 verified, 0 errors
Program compiled successfully
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index e9c2beb4..ba009b83 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" /autoTriggers:1 "%s" > "%t"
// RUN: %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"
// RUN: %diff "%s.expect" "%t"
@@ -35,11 +35,11 @@ class Node { }
method Sequence(s: seq<bool>, j: int, b: bool, c: bool) returns (t: seq<bool>)
- requires 10 <= |s|;
- requires 8 <= j && j < |s|;
- ensures |t| == |s|;
- ensures t[8] == s[8] || t[9] == s[9];
- ensures t[j] == b;
+ requires 10 <= |s|
+ requires 8 <= j < |s|
+ ensures |t| == |s|
+ ensures t[8] == s[8] || t[9] == s[9]
+ ensures t[j] == b
{
if (c) {
t := s[j := b];
@@ -49,14 +49,14 @@ class Node { }
method Max0(x: int, y: int) returns (r: int)
- ensures r == (if x < y then y else x);
+ ensures r == (if x < y then y else x)
{
if (x < y) { r := y; } else { r := x; }
}
method Max1(x: int, y: int) returns (r: int)
- ensures r == x || r == y;
- ensures x <= r && y <= r;
+ ensures r == x || r == y
+ ensures x <= r && y <= r
{
r := if x < y then y else x;
}
@@ -122,12 +122,12 @@ class Modifies { method C(b: bool)
modifies this;
- ensures !b ==> x == old(x) && next == old(next);
+ ensures !b ==> x == old(x) && next == old(next)
{
}
method D(p: Modifies, y: int)
- requires p != null;
+ requires p != null
{
if (y == 3) {
p.C(true); // error: may violate modifies clause
@@ -230,15 +230,15 @@ class InitCalls { method Init(y: int)
modifies this;
- ensures z == y;
+ ensures z == y
{
z := y;
}
method InitFromReference(q: InitCalls)
- requires q != null && 15 <= q.z;
+ requires q != null && 15 <= q.z
modifies this;
- ensures p == q;
+ ensures p == q
{
p := q;
}
@@ -265,35 +265,35 @@ class InitCalls { // --------------- some tests with quantifiers and ranges ----------------------
method QuantifierRange0<T>(a: seq<T>, x: T, y: T, N: int)
- requires 0 <= N && N <= |a|;
- requires forall k | 0 <= k && k < N :: a[k] != x;
- requires exists k | 0 <= k && k < N :: a[k] == y;
- ensures forall k :: 0 <= k && k < N ==> a[k] != x; // same as the precondition, but using ==> instead of |
- ensures exists k :: 0 <= k && k < N && a[k] == y; // same as the precondition, but using && instead of |
+ requires 0 <= N <= |a|
+ requires forall k | 0 <= k < N :: a[k] != x
+ requires exists k | 0 <= k < N :: a[k] == y
+ ensures forall k :: 0 <= k < N ==> a[k] != x; // same as the precondition, but using ==> instead of |
+ ensures exists k :: 0 <= k < N && a[k] == y; // same as the precondition, but using && instead of |
{
assert x != y;
}
method QuantifierRange1<T>(a: seq<T>, x: T, y: T, N: int)
- requires 0 <= N && N <= |a|;
- requires forall k :: 0 <= k && k < N ==> a[k] != x;
- requires exists k :: 0 <= k && k < N && a[k] == y;
- ensures forall k | 0 <= k && k < N :: a[k] != x; // same as the precondition, but using | instead of ==>
- ensures exists k | 0 <= k && k < N :: a[k] == y; // same as the precondition, but using | instead of &&
+ requires 0 <= N <= |a|
+ requires forall k :: 0 <= k < N ==> a[k] != x
+ requires exists k :: 0 <= k < N && a[k] == y
+ ensures forall k | 0 <= k < N :: a[k] != x; // same as the precondition, but using | instead of ==>
+ ensures exists k | 0 <= k < N :: a[k] == y; // same as the precondition, but using | instead of &&
{
assert x != y;
}
method QuantifierRange2<T(==)>(a: seq<T>, x: T, y: T, N: int)
- requires 0 <= N && N <= |a|;
- requires exists k | 0 <= k && k < N :: a[k] == y;
- ensures forall k | 0 <= k && k < N :: a[k] == y; // error
+ requires 0 <= N <= |a|
+ requires exists k | 0 <= k < N :: a[k] == y
+ ensures forall k | 0 <= k < N :: a[k] == y; // error
{
assert N != 0;
if (N == 1) {
- assert forall k | a[if 0 <= k && k < N then k else 0] != y :: k < 0 || N <= k; // in this case, the precondition holds trivially
+ assert forall k {:nowarn} | a[if 0 <= k < N then k else 0] != y :: k < 0 || N <= k; // in this case, the precondition holds trivially
}
- if (forall k | 0 <= k && k < N :: a[k] == x) {
+ if (forall k | 0 <= k < N :: a[k] == x) {
assert x == y;
}
}
@@ -301,8 +301,8 @@ method QuantifierRange2<T(==)>(a: seq<T>, x: T, y: T, N: int) // ----------------------- tests that involve sequences of boxes --------
ghost method M(zeros: seq<bool>, Z: bool)
- requires 1 <= |zeros| && Z == false;
- requires forall k :: 0 <= k && k < |zeros| ==> zeros[k] == Z;
+ requires 1 <= |zeros| && Z == false
+ requires forall k :: 0 <= k < |zeros| ==> zeros[k] == Z
{
var x := [Z];
assert zeros[0..1] == [Z];
@@ -312,7 +312,7 @@ class SomeType {
var x: int;
method DoIt(stack: seq<SomeType>)
- requires null !in stack;
+ requires null !in stack
modifies stack;
{
forall n | n in stack {
@@ -333,7 +333,7 @@ method TestSequences0() } else {
assert 2 in s;
assert 0 in s;
- assert exists n :: n in s && -3 <= n && n < 2;
+ assert exists n :: n in s && -3 <= n < 2;
}
assert 7 in s; // error
}
@@ -399,7 +399,7 @@ class Test { function F(b: bool): int
// The if-then-else in the following line was once translated incorrectly,
// incorrectly causing the postcondition to verify
- ensures if b then F(b) == 5 else F(b) == 6;
+ ensures if b then F(b) == 5 else F(b) == 6
{
5
}
@@ -430,10 +430,10 @@ class AttributeTests { }
method testAttributes0() returns (r: AttributeTests)
- ensures {:boolAttr true} true;
- ensures {:boolAttr false} true;
- ensures {:intAttr 0} true;
- ensures {:intAttr 1} true;
+ ensures {:boolAttr true} true
+ ensures {:boolAttr false} true
+ ensures {:intAttr 0} true
+ ensures {:intAttr 1} true
modifies {:boolAttr true} this`f;
modifies {:boolAttr false} this`f;
modifies {:intAttr 0} this`f;
@@ -541,7 +541,7 @@ method TestNotNot() // ----------------------- Assign-such-that statements -------
method AssignSuchThat0(a: int, b: int) returns (x: int, y: int)
- ensures x == a && y == b;
+ ensures x == a && y == b
{
if (*) {
x, y :| a <= x < a + 1 && b + a <= y + a && y <= b;
@@ -635,7 +635,7 @@ method AssignSuchThat9() returns (q: QuiteFinite) function method LetSuchThat_P(x: int): bool
method LetSuchThat0(ghost g: int)
- requires LetSuchThat_P(g);
+ requires LetSuchThat_P(g)
{
var t :| LetSuchThat_P(t); // assign-such-that statement
ghost var u := var q :| LetSuchThat_P(q); q + 1; // let-such-that expression
@@ -710,10 +710,10 @@ class GT { {
if (*) {
P0();
- assert forall x: GT :: x != null ==> !fresh(x); // error: method P2 may have allocated stuff
+ assert forall x: GT {:nowarn} :: x != null ==> !fresh(x); // error: method P2 may have allocated stuff
} else {
P1();
- assert forall x: GT :: x != null ==> !fresh(x); // fine, because the ghost method does not allocate anything
+ assert forall x: GT {:nowarn} :: x != null ==> !fresh(x); // fine, because the ghost method does not allocate anything
}
}
}
@@ -777,20 +777,20 @@ module GenericPick { var x :| x in s; x
}
function SeqPick3<U>(s: seq<U>): U
- requires exists i :: 0 <= i < |s|
+ requires exists i {:nowarn} :: 0 <= i < |s|
{
EquivalentWaysOfSayingSequenceIsNonempty(s); // I wish this wasn't needed; see comment near Seq#Length axioms in DafnyPrelude.bpl
var x :| x in s; x
}
function SeqPick4<U>(s: seq<U>): U
- requires exists i :: 0 <= i < |s|
+ requires exists i {:nowarn} :: 0 <= i < |s|
{
var i :| 0 <= i < |s|; s[i]
}
lemma EquivalentWaysOfSayingSequenceIsNonempty<U>(s: seq<U>)
requires s != []
|| |s| != 0
- || exists i :: 0 <= i < |s|
+ || exists i {:nowarn} :: 0 <= i < |s|
ensures exists x :: x in s
{
assert s[0] in s;
diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect index eee0d4f1..4bd12096 100644 --- a/Test/dafny0/SmallTests.dfy.expect +++ b/Test/dafny0/SmallTests.dfy.expect @@ -107,6 +107,7 @@ Execution trace: (0,0): anon3
SmallTests.dfy(296,2): Error BP5003: A postcondition might not hold on this return path.
SmallTests.dfy(290,10): Related location: This is the postcondition that might not hold.
+SmallTests.dfy(290,40): Related location
Execution trace:
(0,0): anon0
(0,0): anon18_Else
@@ -117,8 +118,8 @@ Execution trace: SmallTests.dfy(338,11): Error: assertion violation
Execution trace:
(0,0): anon0
- (0,0): anon8_Then
- (0,0): anon7
+ (0,0): anon7_Then
+ (0,0): anon6
SmallTests.dfy(345,9): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/TriggerInPredicate.dfy.expect b/Test/dafny0/TriggerInPredicate.dfy.expect index 1cbd4034..b3fb9cc0 100644 --- a/Test/dafny0/TriggerInPredicate.dfy.expect +++ b/Test/dafny0/TriggerInPredicate.dfy.expect @@ -1,5 +1,5 @@ -TriggerInPredicate.dfy(6,32): Info: Not generating triggers for {A(x, y)}.
-TriggerInPredicate.dfy(6,32): Info: Not generating triggers for {z}.
+TriggerInPredicate.dfy(6,32): Info: Not generating triggers for "A(x, y)".
+TriggerInPredicate.dfy(6,32): Info: Not generating triggers for "z".
TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.
TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.
diff --git a/Test/dafny0/columns.dfy b/Test/dafny0/columns.dfy index e36142be..72c9ab81 100644 --- a/Test/dafny0/columns.dfy +++ b/Test/dafny0/columns.dfy @@ -3,8 +3,10 @@ // Dafny counts columns from 0, but Boogie from one, so for a while there were small bugs with that.
+predicate P(x: int)
+
static method A(x:int) requires x > 0 { // error os 's'
- assert (forall y :: y > x ==> y > 100); // error on '('
+ assert (forall y: int :: P(y)); // error on '('
assert x != 1; // error on '!'
assert x in {}; // error on 'i'
}
diff --git a/Test/dafny0/columns.dfy.expect b/Test/dafny0/columns.dfy.expect index 295ca351..0a99be69 100644 --- a/Test/dafny0/columns.dfy.expect +++ b/Test/dafny0/columns.dfy.expect @@ -1,18 +1,12 @@ -columns.dfy(6,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
-columns.dfy(7,9): Error: assertion violation
+columns.dfy(8,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+columns.dfy(9,9): Error: assertion violation
Execution trace:
(0,0): anon0
- (0,0): anon3_Then
- (0,0): anon2
-columns.dfy(8,11): Error: assertion violation
+columns.dfy(10,11): Error: assertion violation
Execution trace:
(0,0): anon0
- (0,0): anon3_Then
- (0,0): anon2
-columns.dfy(9,11): Error: assertion violation
+columns.dfy(11,11): Error: assertion violation
Execution trace:
(0,0): anon0
- (0,0): anon3_Then
- (0,0): anon2
-Dafny program verifier finished with 1 verified, 3 errors
+Dafny program verifier finished with 2 verified, 3 errors
diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy b/Test/dafny0/snapshots/Snapshots5.run.dfy index e0f3b16b..096df53c 100644 --- a/Test/dafny0/snapshots/Snapshots5.run.dfy +++ b/Test/dafny0/snapshots/Snapshots5.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots5.dfy" > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots5.dfy" /autoTriggers:1 > "%t"
// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy.expect b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect index 8148a8cf..8cc44882 100644 --- a/Test/dafny0/snapshots/Snapshots5.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect @@ -1,3 +1,7 @@ +Snapshots5.v0.dfy(10,12): Warning: /!\ No terms found to trigger on.
+Snapshots5.v0.dfy(13,10): Warning: /!\ No terms found to trigger on.
+Snapshots5.v0.dfy(20,12): Warning: /!\ No terms found to trigger on.
+Snapshots5.v0.dfy(26,11): Warning: /!\ No terms found to trigger on.
Processing command (at Snapshots5.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;
@@ -10,6 +14,11 @@ Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#5: bool :: tru >>> DoNothingToAssert
Dafny program verifier finished with 3 verified, 0 errors
+Snapshots5.v1.dfy(10,12): Warning: /!\ No terms found to trigger on.
+Snapshots5.v1.dfy(13,10): Warning: /!\ No terms found to trigger on.
+Snapshots5.v1.dfy(20,12): Warning: /!\ No terms found to trigger on.
+Snapshots5.v1.dfy(22,10): Warning: /!\ No terms found to trigger on.
+Snapshots5.v1.dfy(27,11): Warning: /!\ No terms found to trigger on.
Processing command (at Snapshots5.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;
diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy index 0940d9e7..374555b0 100644 --- a/Test/dafny1/FindZero.dfy +++ b/Test/dafny1/FindZero.dfy @@ -3,7 +3,7 @@ method FindZero(a: array<int>) returns (r: int)
requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
- requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
+ requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
ensures 0 <= r ==> r < a.Length && a[r] == 0;
ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;
{
@@ -20,7 +20,7 @@ method FindZero(a: array<int>) returns (r: int) lemma Lemma(a: array<int>, k: int, m: int)
requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
- requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
+ requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
requires 0 <= k;
requires k < a.Length ==> m <= a[k];
ensures forall i :: k <= i < k+m && i < a.Length ==> a[i] != 0;
@@ -36,7 +36,7 @@ lemma Lemma(a: array<int>, k: int, m: int) method FindZero_GhostLoop(a: array<int>) returns (r: int)
requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
- requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
+ requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
ensures 0 <= r ==> r < a.Length && a[r] == 0;
ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;
{
@@ -63,7 +63,7 @@ method FindZero_GhostLoop(a: array<int>) returns (r: int) method FindZero_Assert(a: array<int>) returns (r: int)
requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
- requires forall i :: 0 <= i-1 && i < a.Length ==> a[i-1]-1 <= a[i];
+ requires forall i {:nowarn} :: 0 <= i-1 && i < a.Length ==> a[i-1]-1 <= a[i];
ensures 0 <= r ==> r < a.Length && a[r] == 0;
ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;
{
diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy index 319bb8d0..bd654db5 100644 --- a/Test/dafny1/MoreInduction.dfy +++ b/Test/dafny1/MoreInduction.dfy @@ -83,12 +83,12 @@ lemma LemmaOne(n: int) {
}
-lemma LemmaAll_Neg()
- ensures forall n :: NegFac(-n) <= -1; // error: fails to verify because of the minus in the trigger
+lemma LemmaAll_Neg() //FIXME I don't understand the comment below; what trigger?
+ ensures forall n {:nowarn} :: NegFac(-n) <= -1; // error: fails to verify because of the minus in the trigger
{
}
-lemma LemmaOne_Neg(n: int)
+lemma LemmaOne_Neg(n: int) //FIXME What trigger?
ensures NegFac(-n) <= -1; // error: fails to verify because of the minus in the trigger
{
}
diff --git a/Test/dafny1/MoreInduction.dfy.expect b/Test/dafny1/MoreInduction.dfy.expect index 5de0ace6..7da5e2ec 100644 --- a/Test/dafny1/MoreInduction.dfy.expect +++ b/Test/dafny1/MoreInduction.dfy.expect @@ -1,5 +1,6 @@ MoreInduction.dfy(78,0): Error BP5003: A postcondition might not hold on this return path.
MoreInduction.dfy(77,10): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(77,32): Related location
Execution trace:
(0,0): anon0
MoreInduction.dfy(83,0): Error BP5003: A postcondition might not hold on this return path.
@@ -8,6 +9,7 @@ Execution trace: (0,0): anon0
MoreInduction.dfy(88,0): Error BP5003: A postcondition might not hold on this return path.
MoreInduction.dfy(87,10): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(87,43): Related location
Execution trace:
(0,0): anon0
MoreInduction.dfy(93,0): Error BP5003: A postcondition might not hold on this return path.
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]) {
diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy index 2aa14db7..72250f99 100644 --- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy +++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy @@ -164,7 +164,7 @@ class Node { invariant 0 <= t < h && Nexxxt(t, S) == tortoise && Nexxxt(h, S) == hare;
// What follows of the invariant is for proving termination:
invariant h == 1 + 2*t && t <= A + B;
- invariant forall k :: 0 <= k < t ==> Nexxxt(k, S) != Nexxxt(1+2*k, S);
+ invariant forall k {:nowarn} :: 0 <= k < t ==> Nexxxt(k, S) != Nexxxt(1+2*k, S);
decreases A + B - t;
{
if hare == null || hare.next == null {
@@ -225,7 +225,7 @@ class Node { requires 0 <= a && 1 <= b;
requires forall k,l :: 0 <= k < l < a ==> Nexxxt(k, S) != Nexxxt(l, S);
requires Nexxxt(a, S) == null || Nexxxt(a, S).Nexxxt(b, S) == Nexxxt(a, S);
- ensures exists T :: 0 <= T < a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S);
+ ensures exists T {:nowarn} :: 0 <= T < a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S);
{
if Nexxxt(a, S) == null {
Lemma_NullIsTerminal(1+2*a, S);
diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy index 6bd06965..ea75c196 100644 --- a/Test/dafny3/GenericSort.dfy +++ b/Test/dafny3/GenericSort.dfy @@ -36,7 +36,7 @@ abstract module Sort { requires a != null && 0 <= low <= high <= a.Length
reads a
{
- forall i :: low < i < high ==> O.Leq(a[i-1], a[i])
+ forall i {:nowarn} :: low < i < high ==> O.Leq(a[i-1], a[i])
}
// ...but we show that property to imply all pairs to be sorted. The proof of this
// lemma uses the transitivity property.
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
diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy index d5551d82..bc3b5baf 100644 --- a/Test/vacid0/Composite.dfy +++ b/Test/vacid0/Composite.dfy @@ -68,7 +68,7 @@ class Composite { // sets child.parent to this:
ensures child.parent == this;
// leaves everything in S+U valid:
- ensures (forall c :: c in S+U ==> c.Valid(S+U));
+ ensures (forall c {:autotriggers false} :: c in S+U ==> c.Valid(S+U)); // We can't generate a trigger for this at the moment; if we did, we would still need to prevent TrSplitExpr from translating c in S+U to S[c] || U[c].
{
if (left == null) {
left := child;
diff --git a/Test/wishlist/exists-b-exists-not-b.dfy b/Test/wishlist/exists-b-exists-not-b.dfy index 711c5611..2573b2f2 100644 --- a/Test/wishlist/exists-b-exists-not-b.dfy +++ b/Test/wishlist/exists-b-exists-not-b.dfy @@ -5,6 +5,6 @@ // otherwise, trigger splitting prevents `exists b :: b || not b` from verifying
method M() {
- assert exists b: bool :: b; // WISH
- assert exists b: bool :: !b; // WISH
+ assert exists b : bool {:nowarn} :: b; // WISH
+ assert exists b : bool {:nowarn} :: !b; // WISH
}
|