From 91fa6b7d576a111f39cde20de5d8e612b4d712b5 Mon Sep 17 00:00:00 2001 From: leino Date: Thu, 25 Jun 2015 18:12:53 -0700 Subject: Tried to reduce frame-axiom instantiations by saying the earlier heap must be a "heap anchor". Currently, a heap is an anchor if it produced by a havoc (but not a direct update). --- Test/VerifyThis2015/Problem3.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Test/VerifyThis2015/Problem3.dfy') diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy index 4205035d..10ad2d3a 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" /vcsMaxKeepGoingSplits:5 "%s" > "%t" +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino -- cgit v1.2.3 From 550caf7bc7e6427f26bfb3d24f224e12c6c1c318 Mon Sep 17 00:00:00 2001 From: leino Date: Wed, 1 Jul 2015 13:29:11 -0700 Subject: Fixed bug in BplImp! Improvements in encoding of reads of function values. --- Binaries/DafnyPrelude.bpl | 8 ++++++++ Source/Dafny/Translator.cs | 16 +++++++--------- Test/VerifyThis2015/Problem3.dfy | 2 +- Test/dafny4/NumberRepresentations.dfy | 2 +- 4 files changed, 17 insertions(+), 11 deletions(-) (limited to 'Test/VerifyThis2015/Problem3.dfy') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index dbf9b76c..2ca10f73 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -273,6 +273,8 @@ const unique class._System.set: ClassName; const unique class._System.seq: ClassName; const unique class._System.multiset: ClassName; +function Tclass._System.object(): Ty; + function /*{:never_pattern true}*/ dtype(ref): Ty; // changed from ClassName to Ty function TypeTuple(a: ClassName, b: ClassName): ClassName; @@ -287,6 +289,12 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) } type HandleType; +function SetRef_to_SetBox(s: [ref]bool): Set Box; +axiom (forall s: [ref]bool, bx: Box :: { SetRef_to_SetBox(s)[bx] } + SetRef_to_SetBox(s)[bx] == s[$Unbox(bx): ref]); +axiom (forall s: [ref]bool :: { SetRef_to_SetBox(s) } + $Is(SetRef_to_SetBox(s), TSet(Tclass._System.object()))); + // --------------------------------------------------------------- // -- Datatypes -------------------------------------------------- // --------------------------------------------------------------- diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index c98bd203..78f5c89d 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -5713,11 +5713,9 @@ namespace Microsoft.Dafny { { // forall t1, .., tN+1 : Ty, p: [Heap, Box, ..., Box] Box, heap : Heap, b1, ..., bN : Box - // :: RequriesN(...) ==> ApplyN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) = h[heap, b1, ..., bN] - // - // no precondition for these, but: - // for requires, we add: RequiresN(...) <== r[heap, b1, ..., bN] - // for reads, we could: ReadsN(...)[bx] ==> rd[heap, b1, ..., bN][bx] , but we don't + // :: ApplyN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) == h[heap, b1, ..., bN] + // :: RequiresN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) <== r[heap, b1, ..., bN] + // :: ReadsN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) == rd[heap, b1, ..., bN] Action SelectorSemantics = (selector, selectorTy, selectorVar, selectorVarTy, precond, precondTy) => { Contract.Assert((precond == null) == (precondTy == null)); var bvars = new List(); @@ -5919,7 +5917,7 @@ namespace Microsoft.Dafny { var inner_name = GetClass(td).TypedIdent.Name; string name = "T" + inner_name; // Create the type constructor - { + if (td.Name != "object") { // the type constructor for "object" is in DafnyPrelude.bpl Bpl.Variable tyVarOut = BplFormalVar(null, predef.Ty, false); List args = new List( Enumerable.Range(0, arity).Select(i => @@ -11462,10 +11460,10 @@ namespace Microsoft.Dafny { } var rdvars = new List(); - var o = translator.UnboxIfBoxed(BplBoundVar(varNameGen.FreshId("#o#"), predef.BoxType, rdvars), new ObjectType()); - + var o = BplBoundVar(varNameGen.FreshId("#o#"), predef.RefType, rdvars); Bpl.Expr rdbody = new Bpl.LambdaExpr(e.tok, new List(), rdvars, null, translator.InRWClause(e.tok, o, null, e.Reads.ConvertAll(su.SubstFrameExpr), et, null, null)); + rdbody = translator.FunctionCall(e.tok, "SetRef_to_SetBox", predef.SetType(e.tok, true, predef.BoxType), rdbody); return translator.Lit( translator.FunctionCall(e.tok, BuiltinFunction.AtLayer, predef.HandleType, @@ -14220,7 +14218,7 @@ namespace Microsoft.Dafny { Contract.Requires(b != null); Contract.Ensures(Contract.Result() != null); - if (a == Bpl.Expr.True || b == Bpl.Expr.True || b == Bpl.Expr.False) { + if (a == Bpl.Expr.True || b == Bpl.Expr.True) { return b; } else if (a == Bpl.Expr.False) { return Bpl.Expr.True; diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy index 10ad2d3a..4205035d 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" /vcsMaxKeepGoingSplits:5 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy index 8a94505c..1ebdf64c 100644 --- a/Test/dafny4/NumberRepresentations.dfy +++ b/Test/dafny4/NumberRepresentations.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /vcsMaxKeepGoingSplits:5 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" // We consider a number representation that consists of a sequence of digits. The least -- cgit v1.2.3 From 0d94c8f5795b092372df5a06d6d0f9306d696d9b Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Tue, 21 Jul 2015 11:38:51 -0700 Subject: Update z3 to 4.4. One test had to be edited. --- Binaries/z3.exe | Bin 6343680 -> 11018752 bytes Test/VerifyThis2015/Problem3.dfy | 20 +++++++++++++++++++- Test/VerifyThis2015/Problem3.dfy.expect | 2 +- 3 files changed, 20 insertions(+), 2 deletions(-) (limited to 'Test/VerifyThis2015/Problem3.dfy') diff --git a/Binaries/z3.exe b/Binaries/z3.exe index 72aa6ccd..4e29a0a7 100644 Binary files a/Binaries/z3.exe and b/Binaries/z3.exe differ diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy index 4205035d..21bdd4ed 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" /vcsMaxKeepGoingSplits:5 "%s" > "%t" +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino @@ -92,6 +92,21 @@ class DoublyLinkedList { } Nodes := nodes; } + + function PopMiddle(s: seq, k: nat) : seq + requires k < |s| { + s[..k] + s[k+1..] + } + + predicate Injective(s: seq) { + forall j, k :: 0 <= j < k < |s| ==> s[j] != s[k] + } + + lemma InjectiveAfterPop(s: seq, k: nat) + requires k < |s| + requires Injective(s) + ensures Injective(PopMiddle(s, k)) { } + method Remove(x: Node) returns (ghost k: int) requires Valid() requires x in Nodes && x != Nodes[0] && x != Nodes[|Nodes|-1] // not allowed to remove end nodes; you may think of them as a sentinel nodes @@ -103,8 +118,11 @@ class DoublyLinkedList { k :| 1 <= k < |Nodes|-1 && Nodes[k] == x; x.R.L := x.L; x.L.R := x.R; + + InjectiveAfterPop(Nodes, k); Nodes := Nodes[..k] + Nodes[k+1..]; } + // One might consider have a precondition that says there exists a "k" with the properties given here. // However, we want to be able to refer to "k" in the postcondition as well, so it's convenient to // burden the client with having to pass in "k" as a ghost parameter. This, however, is really no diff --git a/Test/VerifyThis2015/Problem3.dfy.expect b/Test/VerifyThis2015/Problem3.dfy.expect index 4035605c..d3a9554b 100644 --- a/Test/VerifyThis2015/Problem3.dfy.expect +++ b/Test/VerifyThis2015/Problem3.dfy.expect @@ -1,5 +1,5 @@ -Dafny program verifier finished with 15 verified, 0 errors +Dafny program verifier finished with 19 verified, 0 errors Program compiled successfully Running... -- 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/VerifyThis2015/Problem3.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