From f28fa68497352ffb57ab2846da4cc1c1aeaf1968 Mon Sep 17 00:00:00 2001 From: leino Date: Wed, 12 Aug 2015 22:44:50 -0700 Subject: Change the induction heuristic for lemmas to also look in precondition for clues about which parameters to include. As a result, improved many test cases (see, e.g., dafny4/NipkowKlein-chapter7.dfy!) and beautified some others. --- Test/dafny0/Parallel.dfy | 146 +++++++++++++++++++++++------------------------ 1 file changed, 73 insertions(+), 73 deletions(-) (limited to 'Test/dafny0/Parallel.dfy') diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy index 030eb350..e0d6491b 100644 --- a/Test/dafny0/Parallel.dfy +++ b/Test/dafny0/Parallel.dfy @@ -2,13 +2,13 @@ // RUN: %diff "%s.expect" "%t" class C { - var data: int; - var n: nat; - var st: set; + var data: int + var n: nat + var st: set ghost method CLemma(k: int) - requires k != -23; - ensures data < k; // magic, isn't it (or bogus, some would say) + requires k != -23 + ensures data < k // magic, isn't it (or bogus, some would say) } // This method more or less just tests the syntax, resolution, and basic verification @@ -19,31 +19,31 @@ method ParallelStatement_Resolve( S: set, clx: C, cly: C, clk: int ) - requires a != null && null !in spine; - modifies a, spine; + requires a != null && null !in spine + modifies a, spine { - forall (i: int | 0 <= i < a.Length && i % 2 == 0) { + forall i | 0 <= i < a.Length && i % 2 == 0 { a[i] := a[(i + 1) % a.Length] + 3; } - forall (o | o in spine) { + forall o | o in spine { o.st := o.st + Repr; } - forall (x, y | x in S && 0 <= y+x < 100) { + forall x, y | x in S && 0 <= y+x < 100 { Lemma(clx, x, y); // error: precondition does not hold (clx may be null) } - forall (x, y | x in S && 0 <= y+x < 100) { + forall x, y | x in S && 0 <= y+x < 100 { cly.CLemma(x + y); // error: receiver might be null } - forall (p | 0 <= p) - ensures F(p) <= Sum(p) + p - 1; // error (no connection is known between F and Sum) + forall p | 0 <= p + ensures F(p) <= Sum(p) + p - 1 // error (no connection is known between F and Sum) { assert 0 <= G(p); ghost var t; - if (p % 2 == 0) { + if p % 2 == 0 { assert G(p) == F(p+2); // error (there's nothing that gives any relation between F and G) t := p+p; } else { @@ -56,11 +56,11 @@ method ParallelStatement_Resolve( } } -ghost method Lemma(c: C, x: int, y: int) - requires c != null; - ensures c.data <= x+y; -ghost method PowerLemma(x: int, y: int) - ensures Pred(x, y); +lemma Lemma(c: C, x: int, y: int) + requires c != null + ensures c.data <= x+y +lemma PowerLemma(x: int, y: int) + ensures Pred(x, y) function F(x: int): int function G(x: int): nat @@ -71,54 +71,54 @@ function Pred(x: int, y: int): bool // --------------------------------------------------------------------- method M0(S: set) - requires null !in S; - modifies S; - ensures forall o :: o in S ==> o.data == 85; - ensures forall o :: o != null && o !in S ==> o.data == old(o.data); + requires null !in S + modifies S + ensures forall o :: o in S ==> o.data == 85 + ensures forall o :: o != null && o !in S ==> o.data == old(o.data) { - forall (s | s in S) { + forall s | s in S { s.data := 85; } } method M1(S: set, x: C) - requires null !in S && x in S; + requires null !in S && x in S { - forall (s | s in S) - ensures s.data < 100; + forall s | s in S + ensures s.data < 100 { assume s.data == 85; } - if (*) { + if * { assert x.data == 85; // error (cannot be inferred from forall ensures clause) } else { assert x.data < 120; } - forall (s | s in S) - ensures s.data < 70; // error + forall s | s in S + ensures s.data < 70 // error { assume s.data == 85; } } method M2() returns (a: array) - ensures a != null; - ensures forall i,j :: 0 <= i < a.Length/2 <= j < a.Length ==> a[i] < a[j]; + ensures a != null + ensures forall i,j :: 0 <= i < a.Length/2 <= j < a.Length ==> a[i] < a[j] { a := new int[250]; - forall (i: nat | i < 125) { + forall i: nat | i < 125 { a[i] := 423; } - forall (i | 125 <= i < 250) { + forall i | 125 <= i < 250 { a[i] := 300 + i; } } method M4(S: set, k: int) - modifies S; + modifies S { - forall (s | s in S && s != null) { + forall s | s in S && s != null { s.n := k; // error: k might be negative } } @@ -127,25 +127,25 @@ method M5() { if { case true => - forall (x | 0 <= x < 100) { + forall x | 0 <= x < 100 { PowerLemma(x, x); } assert Pred(34, 34); case true => - forall (x,y | 0 <= x < 100 && y == x+1) { + forall x,y | 0 <= x < 100 && y == x+1 { PowerLemma(x, y); } assert Pred(34, 35); case true => - forall (x,y | 0 <= x < y < 100) { + forall x,y | 0 <= x < y < 100 { PowerLemma(x, y); } assert Pred(34, 35); case true => - forall (x | x in set k | 0 <= k < 100) { + forall x | x in set k | 0 <= k < 100 { PowerLemma(x, x); } assert Pred(34, 34); @@ -155,22 +155,22 @@ method M5() method Main() { var a := new int[180]; - forall (i | 0 <= i < 180) { + forall i | 0 <= i < 180 { a[i] := 2*i + 100; } var sq := [0, 0, 0, 2, 2, 2, 5, 5, 5]; - forall (i | 0 <= i < |sq|) { + forall i | 0 <= i < |sq| { a[20+i] := sq[i]; } - forall (t | t in sq) { + forall t | t in sq { a[t] := 1000; } - forall (t,u | t in sq && t < 4 && 10 <= u < 10+t) { + forall t,u | t in sq && t < 4 && 10 <= u < 10+t { a[u] := 6000 + t; } var k := 0; - while (k < 180) { - if (k != 0) { print ", "; } + while k < 180 { + if k != 0 { print ", "; } print a[k]; k := k + 1; } @@ -180,50 +180,50 @@ method Main() method DuplicateUpdate() { var a := new int[180]; var sq := [0, 0, 0, 2, 2, 2, 5, 5, 5]; - if (*) { - forall (t,u | t in sq && 10 <= u < 10+t) { + if * { + forall t,u | t in sq && 10 <= u < 10+t { a[u] := 6000 + t; // error: a[10] (and a[11]) are assigned more than once } } else { - forall (t,u | t in sq && t < 4 && 10 <= u < 10+t) { + forall t,u | t in sq && t < 4 && 10 <= u < 10+t { a[u] := 6000 + t; // with the 't < 4' conjunct in the line above, this is fine } } } -ghost method DontDoMuch(x: int) +lemma DontDoMuch(x: int) { } method OmittedRange() { - forall (x: int) { } // a type is still needed for the bound variable - forall (x) { + forall x: int { } // a type is still needed for the bound variable + forall x { DontDoMuch(x); } } // ----------------------- two-state postconditions --------------------------------- -class TwoState_C { ghost var data: int; } +class TwoState_C { ghost var data: int } // It is not possible to achieve this postcondition in a ghost method, because ghost // 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 :: o != null && fresh(o) method TwoState_Main0() { - forall (x) { TwoState0(x); } + forall x { TwoState0(x); } assert false; // no prob, because the postcondition of TwoState0 implies false } method X_Legit(c: TwoState_C) - requires c != null; - modifies c; + requires c != null + modifies c { c.data := c.data + 1; - forall (x | c.data <= x) - ensures old(c.data) < x; // note that the 'old' refers to the method's initial state + forall x | c.data <= x + ensures old(c.data) < x // note that the 'old' refers to the method's initial state { } } @@ -235,8 +235,8 @@ method X_Legit(c: TwoState_C) // method, not the beginning of the 'forall' statement. method TwoState_Main2() { - forall (x: int) - ensures exists o: TwoState_C :: o != null && fresh(o); + forall x: int + ensures exists o: TwoState_C :: o != null && fresh(o) { TwoState0(x); } @@ -251,8 +251,8 @@ method TwoState_Main2() // statement's effect on the heap is not optimized away. method TwoState_Main3() { - forall (x: int) - ensures exists o: TwoState_C :: o != null && fresh(o); + forall x: int + ensures exists o: TwoState_C :: o != null && fresh(o) { assume false; // (there's no other way to achieve this forall-statement postcondition) } @@ -262,11 +262,11 @@ method TwoState_Main3() // ------- empty forall statement ----------------------------------------- class EmptyForallStatement { - var emptyPar: int; + var emptyPar: int method Empty_Parallel0() - modifies this; - ensures emptyPar == 8; + modifies this + ensures emptyPar == 8 { forall () { this.emptyPar := 8; @@ -274,11 +274,11 @@ class EmptyForallStatement { } function EmptyPar_P(x: int): bool - ghost method EmptyPar_Lemma(x: int) - ensures EmptyPar_P(x); + lemma EmptyPar_Lemma(x: int) + ensures EmptyPar_P(x) method Empty_Parallel1() - ensures EmptyPar_P(8); + ensures EmptyPar_P(8) { forall { EmptyPar_Lemma(8); @@ -288,7 +288,7 @@ class EmptyForallStatement { method Empty_Parallel2() { forall - ensures exists k :: EmptyPar_P(k); + ensures exists k :: EmptyPar_P(k) { var y := 8; assume EmptyPar_P(y); @@ -312,9 +312,9 @@ predicate ThProperty(step: nat, t: Nat, r: nat) case Succ(o) => step>0 && exists ro:nat :: ThProperty(step-1, o, ro) } -ghost method Th(step: nat, t: Nat, r: nat) - requires t.Succ? && ThProperty(step, t, r); +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 :: ThProperty(step-1, t.tail, ro) { } -- cgit v1.2.3 From 95a42a224dff8eae383d93beb37a3da6a28bb0f3 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel 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/dafny0/Comprehensions.dfy | 10 +-- Test/dafny0/DTypes.dfy | 36 ++++----- Test/dafny0/Matrix-OOB.dfy | 2 +- Test/dafny0/Matrix-OOB.dfy.expect | 2 + Test/dafny0/Modules1.dfy | 2 +- Test/dafny0/Parallel.dfy | 10 +-- Test/dafny0/Predicates.dfy | 2 +- Test/dafny0/Predicates.dfy.expect | 2 + Test/dafny0/SeqFromArray.dfy | 6 +- Test/dafny0/SeqFromArray.dfy.expect | 3 - Test/dafny0/SmallTests.dfy | 90 +++++++++++----------- Test/dafny0/SmallTests.dfy.expect | 5 +- Test/dafny0/TriggerInPredicate.dfy.expect | 4 +- Test/dafny0/columns.dfy | 4 +- Test/dafny0/columns.dfy.expect | 16 ++-- Test/dafny0/snapshots/Snapshots5.run.dfy | 2 +- Test/dafny0/snapshots/Snapshots5.run.dfy.expect | 9 +++ Test/dafny1/FindZero.dfy | 8 +- Test/dafny1/MoreInduction.dfy | 6 +- Test/dafny1/MoreInduction.dfy.expect | 2 + Test/dafny1/PriorityQueue.dfy | 32 ++++---- .../COST-verif-comp-2011-4-FloydCycleDetect.dfy | 4 +- Test/dafny3/GenericSort.dfy | 2 +- Test/dafny4/Bug60.dfy | 4 +- Test/dafny4/Bug63.dfy | 4 +- Test/dafny4/Primes.dfy | 8 +- Test/vacid0/Composite.dfy | 2 +- Test/wishlist/exists-b-exists-not-b.dfy | 4 +- 28 files changed, 145 insertions(+), 136 deletions(-) (limited to 'Test/dafny0/Parallel.dfy') 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(s: set) { 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; 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) { var x: object := a; - assert (forall b: CP :: x == b ==> b == null); // follows from type antecedents + assert (forall b: CP {:nowarn} :: x == b ==> b == null); // follows from type antecedents } var a2x: set>; method A2(b: set>) - requires null !in b; + requires null !in b { var x: set := a2x; var y: set := b; @@ -81,7 +81,7 @@ class CP { 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 { } method Theorem0(tree: Tree) - ensures 1 <= LeafCount(tree); + ensures 1 <= LeafCount(tree) { assert (forall t: Tree :: 1 <= LeafCount(t)); } // also make sure it works for an instantiated generic datatype method Theorem1(bt: Tree, it: Tree) - ensures 1 <= LeafCount(bt); - ensures 1 <= LeafCount(it); + ensures 1 <= LeafCount(bt) + ensures 1 <= LeafCount(it) { assert (forall t: Tree :: 1 <= LeafCount(t)); assert (forall t: Tree :: 1 <= LeafCount(t)); } method NotATheorem0(tree: Tree) - ensures LeafCount(tree) % 2 == 1; + ensures LeafCount(tree) % 2 == 1 { assert (forall t: Tree :: LeafCount(t) % 2 == 1); // error: fails for Branch case } method NotATheorem1(tree: Tree) - ensures 2 <= LeafCount(tree); + ensures 2 <= LeafCount(tree) { assert (forall t: Tree :: 2 <= LeafCount(t)); // error: fails for Leaf case } @@ -140,22 +140,22 @@ class DatatypeInduction { // ----- here is a test for induction over integers method IntegerInduction_Succeeds(a: array) - 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) - 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>, b: array>) - requires a != null && b != null; + requires a != null && b != null // If P were a known type, then it would also be known that P and P // 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(m: map) lemma m(m: map) - ensures exists m :: p(var m : map := m; m); + ensures exists m {:nowarn} :: p(var m : map := 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, c: array, 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, c: array, 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, j: int, b: bool, c: bool) returns (t: seq) - 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(a: seq, 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(a: seq, 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(a: seq, 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(a: seq, x: T, y: T, N: int) // ----------------------- tests that involve sequences of boxes -------- ghost method M(zeros: seq, 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) - 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(s: seq): 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(s: seq): U - requires exists i :: 0 <= i < |s| + requires exists i {:nowarn} :: 0 <= i < |s| { var i :| 0 <= i < |s|; s[i] } lemma EquivalentWaysOfSayingSequenceIsNonempty(s: seq) 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 $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 $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) 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) returns (r: int) lemma Lemma(a: array, 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, k: int, m: int) method FindZero_GhostLoop(a: array) 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) returns (r: int) method FindZero_Assert(a: array) 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) 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 } -- cgit v1.2.3 From 91cee1c2028f9ad995df863f2a4568d95f4ea1a8 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Mon, 28 Mar 2016 12:02:37 -0700 Subject: Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requires it. Don't use pretty warning signs since we can't diff them correctly in the test output from the test run. --- Source/Dafny/DafnyOptions.cs | 6 ++-- Source/DafnyServer/Utilities.cs | 2 +- Test/VSI-Benchmarks/b8.dfy | 2 +- Test/VerifyThis2015/Problem3.dfy | 2 +- Test/cloudmake/CloudMake-CachedBuilds.dfy | 2 +- Test/cloudmake/CloudMake-ConsistentBuilds.dfy | 2 +- Test/cloudmake/CloudMake-ParallelBuilds.dfy | 2 +- Test/dafny0/Basics.dfy | 2 +- Test/dafny0/Calculations.dfy | 2 +- Test/dafny0/Compilation.dfy | 2 +- Test/dafny0/ForallCompilation.dfy | 2 +- Test/dafny0/Fuel.dfy | 2 +- Test/dafny0/LetExpr.dfy | 2 +- Test/dafny0/LetExpr.dfy.expect | 1 + Test/dafny0/LhsDuplicates.dfy | 2 +- Test/dafny0/Parallel.dfy | 2 +- Test/dafny0/SmallTests.dfy.expect | 1 + Test/dafny1/MoreInduction.dfy | 2 +- Test/dafny1/SchorrWaite-stages.dfy | 2 +- Test/dafny1/SchorrWaite.dfy | 2 +- Test/dafny1/Substitution.dfy | 2 +- Test/dafny1/UltraFilter.dfy | 2 +- Test/dafny2/SnapshotableTrees.dfy | 2 +- Test/dafny3/Filter.dfy | 2 +- Test/dafny4/GHC-MergeSort.dfy | 2 +- Test/dafny4/NumberRepresentations.dfy | 2 +- Test/dafny4/Primes.dfy | 2 +- Test/server/simple-session.transcript.expect | 41 +++++++++++++++++++++++++++ Test/vstte2012/BreadthFirstSearch.dfy | 2 +- 29 files changed, 71 insertions(+), 28 deletions(-) (limited to 'Test/dafny0/Parallel.dfy') diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index f3b38a84..607090eb 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -66,7 +66,7 @@ namespace Microsoft.Dafny public bool AllowGlobals = false; public bool CountVerificationErrors = true; public bool Optimize = false; - public bool AutoTriggers = false; + public bool AutoTriggers = true; public bool RewriteFocalPredicates = true; public bool PrintTooltips = false; public bool PrintStats = false; @@ -386,8 +386,8 @@ namespace Microsoft.Dafny 1 (default) - If preprocessing succeeds, set exit code to the number of verification errors. /autoTriggers: - 0 (default) - Do not generate {:trigger} annotations for user-level quantifiers. - 1 - Add a {:trigger} to each user-level quantifier. Existing + 0 - Do not generate {:trigger} annotations for user-level quantifiers. + 1 (default) - Add a {:trigger} to each user-level quantifier. Existing annotations are preserved. /rewriteFocalPredicates: 0 - Don't rewrite predicates in the body of prefix lemmas. diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index 30d779e7..48bea01a 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -51,7 +51,7 @@ namespace Microsoft.Dafny { DafnyOptions.O.VerifySnapshots = 2; // Use caching DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount / 2); // Don't use too many cores DafnyOptions.O.PrintTooltips = true; // Dump tooptips (ErrorLevel.Info) to stdout - DafnyOptions.O.UnicodeOutput = true; // Use pretty warning signs + //DafnyOptions.O.UnicodeOutput = true; // Use pretty warning signs DafnyOptions.O.TraceProofObligations = true; // Show which method is being verified, but don't show duration of verification } else { throw new ServerException("Invalid command line options"); diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index ea1911fe..a44ff5c3 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny /compile:0 /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Benchmark 8 diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy index 21bdd4ed..60506a33 100644 --- a/Test/VerifyThis2015/Problem3.dfy +++ b/Test/VerifyThis2015/Problem3.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino diff --git a/Test/cloudmake/CloudMake-CachedBuilds.dfy b/Test/cloudmake/CloudMake-CachedBuilds.dfy index 9e1b511e..5f16da90 100644 --- a/Test/cloudmake/CloudMake-CachedBuilds.dfy +++ b/Test/cloudmake/CloudMake-CachedBuilds.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This module proves the correctness of the algorithms. It leaves a number of things undefined. diff --git a/Test/cloudmake/CloudMake-ConsistentBuilds.dfy b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy index 6d86607b..c2fa4205 100644 --- a/Test/cloudmake/CloudMake-ConsistentBuilds.dfy +++ b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" /******* State *******/ diff --git a/Test/cloudmake/CloudMake-ParallelBuilds.dfy b/Test/cloudmake/CloudMake-ParallelBuilds.dfy index 07cae317..5cc70994 100644 --- a/Test/cloudmake/CloudMake-ParallelBuilds.dfy +++ b/Test/cloudmake/CloudMake-ParallelBuilds.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This module proves the correctness of the algorithms. It leaves a number of things undefined. diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index 89b0f02a..7b8b632b 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.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:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class Global { diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy index a7c8e06c..eb4ff1b9 100644 --- a/Test/dafny0/Calculations.dfy +++ b/Test/dafny0/Calculations.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:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy index 7a443e47..213ace54 100644 --- a/Test/dafny0/Compilation.dfy +++ b/Test/dafny0/Compilation.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %dafny /compile:3 /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // The tests in this file are designed to run through the compiler. They contain diff --git a/Test/dafny0/ForallCompilation.dfy b/Test/dafny0/ForallCompilation.dfy index c812983a..4d89f70d 100644 --- a/Test/dafny0/ForallCompilation.dfy +++ b/Test/dafny0/ForallCompilation.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Test/dafny0/Fuel.dfy b/Test/dafny0/Fuel.dfy index 6347e134..a768db02 100644 --- a/Test/dafny0/Fuel.dfy +++ b/Test/dafny0/Fuel.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:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" module TestModule1 { diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy index 000fce53..6a0ca66b 100644 --- a/Test/dafny0/LetExpr.dfy +++ b/Test/dafny0/LetExpr.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:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/LetExpr.dfy.expect b/Test/dafny0/LetExpr.dfy.expect index f0f51274..8f365da3 100644 --- a/Test/dafny0/LetExpr.dfy.expect +++ b/Test/dafny0/LetExpr.dfy.expect @@ -35,5 +35,6 @@ Execution trace: (0,0): anon10_Then Dafny program verifier finished with 39 verified, 9 errors +LetExpr.dfy.tmp.dprint.dfy(162,2): Warning: /!\ No terms found to trigger on. Dafny program verifier finished with 0 verified, 0 errors diff --git a/Test/dafny0/LhsDuplicates.dfy b/Test/dafny0/LhsDuplicates.dfy index 6a84c5a5..8a57f6ce 100644 --- a/Test/dafny0/LhsDuplicates.dfy +++ b/Test/dafny0/LhsDuplicates.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:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class MyClass { diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy index 93a16475..00a1514c 100644 --- a/Test/dafny0/Parallel.dfy +++ b/Test/dafny0/Parallel.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:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class C { diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect index 6161c3dd..746e978a 100644 --- a/Test/dafny0/SmallTests.dfy.expect +++ b/Test/dafny0/SmallTests.dfy.expect @@ -197,5 +197,6 @@ Execution trace: (0,0): anon0 Dafny program verifier finished with 104 verified, 35 errors +SmallTests.dfy.tmp.dprint.dfy(369,4): Warning: /!\ No trigger covering all quantified variables found. Dafny program verifier finished with 0 verified, 0 errors diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy index bd654db5..2b5187a4 100644 --- a/Test/dafny1/MoreInduction.dfy +++ b/Test/dafny1/MoreInduction.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" datatype List = Nil | Cons(Node, List) diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy index 0eaed68c..a6e5e3aa 100644 --- a/Test/dafny1/SchorrWaite-stages.dfy +++ b/Test/dafny1/SchorrWaite-stages.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Schorr-Waite algorithms, written and verified in Dafny. diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy index 50210eb1..b0877f9f 100644 --- a/Test/dafny1/SchorrWaite.dfy +++ b/Test/dafny1/SchorrWaite.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy index da64d004..b9c83aff 100644 --- a/Test/dafny1/Substitution.dfy +++ b/Test/dafny1/Substitution.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" datatype List = Nil | Cons(Expr, List) diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy index a32e6e0b..7ac4e749 100644 --- a/Test/dafny1/UltraFilter.dfy +++ b/Test/dafny1/UltraFilter.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // ultra filter diff --git a/Test/dafny2/SnapshotableTrees.dfy b/Test/dafny2/SnapshotableTrees.dfy index 2bdfb83b..033c5db0 100644 --- a/Test/dafny2/SnapshotableTrees.dfy +++ b/Test/dafny2/SnapshotableTrees.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:2 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:2 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino, September 2011. diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy index 4f8b35ec..7473a580 100644 --- a/Test/dafny3/Filter.dfy +++ b/Test/dafny3/Filter.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" codatatype Stream = Cons(head: T, tail: Stream) diff --git a/Test/dafny4/GHC-MergeSort.dfy b/Test/dafny4/GHC-MergeSort.dfy index 976b8a27..24903d87 100644 --- a/Test/dafny4/GHC-MergeSort.dfy +++ b/Test/dafny4/GHC-MergeSort.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy index 0d6cffa1..c15f4987 100644 --- a/Test/dafny4/NumberRepresentations.dfy +++ b/Test/dafny4/NumberRepresentations.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // We consider a number representation that consists of a sequence of digits. The least diff --git a/Test/dafny4/Primes.dfy b/Test/dafny4/Primes.dfy index fd64b45e..0c2a64dd 100644 --- a/Test/dafny4/Primes.dfy +++ b/Test/dafny4/Primes.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" predicate IsPrime(n: int) diff --git a/Test/server/simple-session.transcript.expect b/Test/server/simple-session.transcript.expect index 1aadca7f..a5f841bc 100644 --- a/Test/server/simple-session.transcript.expect +++ b/Test/server/simple-session.transcript.expect @@ -346,6 +346,7 @@ transcript(10,27): Error: invalid UnaryExpression Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -366,6 +367,7 @@ Execution trace: Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -383,6 +385,7 @@ Verifying Impl$$_module.__default.M_k ... Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -406,6 +409,7 @@ transcript(12,0): Error: invalid UpdateStmt Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -423,6 +427,7 @@ Verifying Impl$$_module.__default.M_k ... Verification completed successfully! [SUCCESS] [[DAFNY-SERVER: EOM]] transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -498,6 +503,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -538,6 +547,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -584,6 +597,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -638,6 +655,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -685,6 +706,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -729,6 +754,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -796,6 +825,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -861,6 +894,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... @@ -905,6 +942,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the ' transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Warning: /!\ No terms found to trigger on. +transcript(20,9): Warning: /!\ No terms found to trigger on. +transcript(29,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: /!\ No terms found to trigger on. Verifying CheckWellformed$$_module.__default.A ... Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A... diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy index b111a438..375f4a09 100644 --- a/Test/vstte2012/BreadthFirstSearch.dfy +++ b/Test/vstte2012/BreadthFirstSearch.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:10 "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:10 /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class BreadthFirstSearch -- cgit v1.2.3