From 3f886d1789d50400ffba2befdc2ae0e8d5c79cbe Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 23 Jul 2015 11:57:19 -0700 Subject: Fix: Unify column numbers in Dafny's errors Dafny counts from 0, but Boogie counts from 1. Tokens are 1-based. Thus when we print tokens, we need to decrement the column number. This was done for resolver errors, but not for verification or parsing errors. In addition, parsing errors were inconsistent with resolution errors case-wise. Unfortunately, the fix affects the output of many tests. --- Test/dafny0/CoinductiveProofs.dfy.expect | 42 ++++++++++++++++---------------- 1 file changed, 21 insertions(+), 21 deletions(-) (limited to 'Test/dafny0/CoinductiveProofs.dfy.expect') diff --git a/Test/dafny0/CoinductiveProofs.dfy.expect b/Test/dafny0/CoinductiveProofs.dfy.expect index 12ce2f01..2a5a2b0b 100644 --- a/Test/dafny0/CoinductiveProofs.dfy.expect +++ b/Test/dafny0/CoinductiveProofs.dfy.expect @@ -1,48 +1,48 @@ -CoinductiveProofs.dfy(29,12): Error: assertion violation -CoinductiveProofs.dfy(13,17): Related location +CoinductiveProofs.dfy(29,11): Error: assertion violation +CoinductiveProofs.dfy(13,16): Related location Execution trace: (0,0): anon0 (0,0): anon5_Then (0,0): anon6_Then -CoinductiveProofs.dfy(59,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(58,11): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(54,3): Related location +CoinductiveProofs.dfy(59,0): Error BP5003: A postcondition might not hold on this return path. +CoinductiveProofs.dfy(58,10): Related location: This is the postcondition that might not hold. +CoinductiveProofs.dfy(54,2): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -CoinductiveProofs.dfy(74,12): Error: assertion violation -CoinductiveProofs.dfy(54,3): Related location +CoinductiveProofs.dfy(74,11): Error: assertion violation +CoinductiveProofs.dfy(54,2): Related location Execution trace: (0,0): anon0 (0,0): anon5_Then (0,0): anon6_Then -CoinductiveProofs.dfy(91,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(90,11): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(80,3): Related location +CoinductiveProofs.dfy(91,0): Error BP5003: A postcondition might not hold on this return path. +CoinductiveProofs.dfy(90,10): Related location: This is the postcondition that might not hold. +CoinductiveProofs.dfy(80,2): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -CoinductiveProofs.dfy(100,12): Error: assertion violation -CoinductiveProofs.dfy(80,3): Related location +CoinductiveProofs.dfy(100,11): Error: assertion violation +CoinductiveProofs.dfy(80,2): Related location Execution trace: (0,0): anon0 (0,0): anon5_Then (0,0): anon6_Then -CoinductiveProofs.dfy(111,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(110,11): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(106,3): Related location +CoinductiveProofs.dfy(111,0): Error BP5003: A postcondition might not hold on this return path. +CoinductiveProofs.dfy(110,10): Related location: This is the postcondition that might not hold. +CoinductiveProofs.dfy(106,2): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -CoinductiveProofs.dfy(150,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(149,22): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(4,24): Related location +CoinductiveProofs.dfy(150,0): Error BP5003: A postcondition might not hold on this return path. +CoinductiveProofs.dfy(149,21): Related location: This is the postcondition that might not hold. +CoinductiveProofs.dfy(4,23): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -CoinductiveProofs.dfy(156,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(155,22): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(4,24): Related location +CoinductiveProofs.dfy(156,0): Error BP5003: A postcondition might not hold on this return path. +CoinductiveProofs.dfy(155,21): Related location: This is the postcondition that might not hold. +CoinductiveProofs.dfy(4,23): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -- cgit v1.2.3 From 1885f7d7d1fb9bd6ceb8220450dbb5d890501337 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 2 Oct 2015 15:26:56 -0700 Subject: Hover text includes #[_k-1] suffix for terms rewritten in prefix predicates/lemmas (this fixes an item from the wishlist). Include in hover text the extreme predicates for which an extreme lemmas has been rewritten (but don't include ==# in this list--or should it perhaps be included?). Under a (temporary) switch /rewriteFocalPredicates, each use of a focal predicate P in a prefix lemma is rewritten into P#[_k-1]. --- Source/Dafny/Cloner.cs | 91 ++++++++++++++++++---- Source/Dafny/DafnyOptions.cs | 27 +++++-- Source/Dafny/Resolver.cs | 16 +++- Test/dafny0/CoinductiveProofs.dfy | 61 ++++++++++++++- Test/dafny0/CoinductiveProofs.dfy.expect | 65 +++++++++++----- Test/wishlist/tooltips-on-inductive-lemmas.dfy | 12 --- .../tooltips-on-inductive-lemmas.dfy.expect | 7 -- 7 files changed, 214 insertions(+), 65 deletions(-) delete mode 100644 Test/wishlist/tooltips-on-inductive-lemmas.dfy delete mode 100644 Test/wishlist/tooltips-on-inductive-lemmas.dfy.expect (limited to 'Test/dafny0/CoinductiveProofs.dfy.expect') diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index c94c697d..45d8a2c9 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -715,7 +715,7 @@ namespace Microsoft.Dafny { protected readonly Expression k; protected readonly ErrorReporter reporter; - readonly string suffix; + protected readonly string suffix; protected FixpointCloner(Expression k, ErrorReporter reporter) { Contract.Requires(k != null); @@ -724,6 +724,18 @@ namespace Microsoft.Dafny this.reporter = reporter; this.suffix = string.Format("#[{0}]", Printer.ExprToString(k)); } + protected Expression CloneCallAndAddK(FunctionCallExpr e) { + Contract.Requires(e != null); + var receiver = CloneExpr(e.Receiver); + var args = new List(); + args.Add(k); + foreach (var arg in e.Args) { + args.Add(CloneExpr(arg)); + } + var fexp = new FunctionCallExpr(Tok(e.tok), e.Name + "#", receiver, e.OpenParen, args); + reporter.Info(MessageSource.Cloner, e.tok, e.Name + suffix); + return fexp; + } } /// @@ -733,6 +745,7 @@ namespace Microsoft.Dafny /// precondition (resp. postcondition) of the inductive lemma's (resp. colemma's) corresponding prefix lemma. /// It is assumed that the source expression has been resolved. Note, the "k" given to the constructor /// is not cloned with each use; it is simply used as is. + /// The resulting expression needs to be resolved by the caller. /// class FixpointLemmaSpecificationSubstituter : FixpointCloner { @@ -756,15 +769,7 @@ namespace Microsoft.Dafny } else if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; if (friendlyCalls.Contains(e)) { - var receiver = CloneExpr(e.Receiver); - var args = new List(); - args.Add(k); - foreach (var arg in e.Args) { - args.Add(CloneExpr(arg)); - } - var fexp = new FunctionCallExpr(Tok(e.tok), e.Name + "#", receiver, e.OpenParen, args); - reporter.Info(MessageSource.Cloner, e.tok, e.Name); - return fexp; + return CloneCallAndAddK(e); } } else if (expr is BinaryExpr && isCoContext) { var e = (BinaryExpr)expr; @@ -774,7 +779,7 @@ namespace Microsoft.Dafny var B = CloneExpr(e.E1); var teq = new TernaryExpr(Tok(e.tok), op, k, A, B); var opString = op == TernaryExpr.Opcode.PrefixEqOp ? "==" : "!="; - reporter.Info(MessageSource.Cloner, e.tok, opString); + reporter.Info(MessageSource.Cloner, e.tok, opString + suffix); return teq; } } @@ -803,19 +808,77 @@ namespace Microsoft.Dafny } /// - /// The task of the FixpointLemmaBodyCloner is to fill in the implicit _k-1 arguments in recursive inductive/co-lemma calls. + /// The task of the FixpointLemmaBodyCloner is to fill in the implicit _k-1 arguments in recursive inductive/co-lemma calls + /// and in calls to the focal predicates. /// The source statement and the given "k" are assumed to have been resolved. /// class FixpointLemmaBodyCloner : FixpointCloner { readonly FixpointLemma context; - public FixpointLemmaBodyCloner(FixpointLemma context, Expression k, ErrorReporter reporter) + readonly ISet focalPredicates; + public FixpointLemmaBodyCloner(FixpointLemma context, Expression k, ISet focalPredicates, ErrorReporter reporter) : base(k, reporter) { Contract.Requires(context != null); Contract.Requires(k != null); Contract.Requires(reporter != null); this.context = context; + this.focalPredicates = focalPredicates; + } + public override Expression CloneExpr(Expression expr) { + if (DafnyOptions.O.RewriteFocalPredicates) { + if (expr is FunctionCallExpr) { + var e = (FunctionCallExpr)expr; +#if DEBUG_PRINT + if (e.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => e.Function.Name == p.Name + "#")) { + Console.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(e)); + } +#endif + // Note, we don't actually ever get here, because all calls will have been parsed as ApplySuffix. + // However, if something changes in the future (for example, some rewrite that changing an ApplySuffix + // to its resolved FunctionCallExpr), then we do want this code, so with the hope of preventing + // some error in the future, this case is included. (Of course, it is currently completely untested!) + var f = e.Function as FixpointPredicate; + if (f != null && focalPredicates.Contains(f)) { +#if DEBUG_PRINT + var r = CloneCallAndAddK(e); + Console.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(r)); + return r; +#else + return CloneCallAndAddK(e); +#endif + } + } else if (expr is ApplySuffix) { + var apply = (ApplySuffix)expr; + if (!apply.WasResolved()) { + // Since we're assuming the enclosing statement to have been resolved, this ApplySuffix must + // be part of an ExprRhs that actually designates a method call. Such an ApplySuffix does + // not get listed as being resolved, but its components (like its .Lhs) are resolved. + var mse = (MemberSelectExpr)apply.Lhs.Resolved; + Contract.Assume(mse.Member is Method); + } else { + var fce = apply.Resolved as FunctionCallExpr; + if (fce != null) { +#if DEBUG_PRINT + if (fce.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => fce.Function.Name == p.Name + "#")) { + Console.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(fce)); + } +#endif + var f = fce.Function as FixpointPredicate; + if (f != null && focalPredicates.Contains(f)) { +#if DEBUG_PRINT + var r = CloneCallAndAddK(fce); + Console.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(r)); + return r; +#else + return CloneCallAndAddK(fce); +#endif + } + } + } + } + } + return base.CloneExpr(expr); } public override AssignmentRhs CloneRHS(AssignmentRhs rhs) { var r = rhs as ExprRhs; @@ -839,7 +902,7 @@ namespace Microsoft.Dafny apply.Args.ForEach(arg => args.Add(CloneExpr(arg))); var applyClone = new ApplySuffix(Tok(apply.tok), lhsClone, args); var c = new ExprRhs(applyClone); - reporter.Info(MessageSource.Cloner, apply.Lhs.tok, mse.Member.Name); + reporter.Info(MessageSource.Cloner, apply.Lhs.tok, mse.Member.Name + suffix); return c; } } diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 59d0eb2c..2d8756d2 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -65,11 +65,12 @@ namespace Microsoft.Dafny public bool AllowGlobals = false; public bool CountVerificationErrors = true; public bool Optimize = false; - public bool AutoTriggers = false; + public bool AutoTriggers = false; + public bool RewriteFocalPredicates = false; public bool PrintTooltips = false; public bool PrintStats = false; public bool PrintFunctionCallGraph = false; - public bool WarnShadowing = false; + public bool WarnShadowing = false; public bool IronDafny = #if ENABLE_IRONDAFNY true @@ -216,12 +217,20 @@ namespace Microsoft.Dafny case "printTooltips": PrintTooltips = true; - return true; + return true; + + case "autoTriggers": { + int autoTriggers = 0; + if (ps.GetNumericArgument(ref autoTriggers, 2)) { + AutoTriggers = autoTriggers == 1; + } + return true; + } - case "autoTriggers": { - int autoTriggers = 0; - if (ps.GetNumericArgument(ref autoTriggers, 2)) { - AutoTriggers = autoTriggers == 1; + case "rewriteFocalPredicates": { + int rewriteFocalPredicates = 0; + if (ps.GetNumericArgument(ref rewriteFocalPredicates, 2)) { + RewriteFocalPredicates = rewriteFocalPredicates == 1; } return true; } @@ -369,6 +378,10 @@ namespace Microsoft.Dafny 0 (default) - Do not generate {:trigger} annotations for user-level quantifiers. 1 - Add a {:trigger} to each user-level quantifier. Existing annotations are preserved. + /rewriteFocalPredicates: + 0 (default) - Don't rewrite predicates in the body of prefix lemmas. + 1 - In the body of prefix lemmas, rewrite any use of a focal predicate + P to P#[_k-1]. /optimize Produce optimized C# code, meaning: - selects optimized C# prelude by passing /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 36464925..7a540722 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1565,6 +1565,7 @@ namespace Microsoft.Dafny continue; // something went wrong during registration of the prefix lemma (probably a duplicated fixpoint-lemma name) } var k = prefixLemma.Ins[0]; + var focalPredicates = new HashSet(); if (com is CoLemma) { // compute the postconditions of the prefix lemma Contract.Assume(prefixLemma.Ens.Count == 0); // these are not supposed to have been filled in before @@ -1574,6 +1575,12 @@ namespace Microsoft.Dafny var subst = new FixpointLemmaSpecificationSubstituter(coConclusions, new IdentifierExpr(k.tok, k.Name), this.reporter, true); var post = subst.CloneExpr(p.E); prefixLemma.Ens.Add(new MaybeFreeExpression(post, p.IsFree)); + foreach (var e in coConclusions) { + var fce = e as FunctionCallExpr; + if (fce != null) { // the other possibility is that "e" is a BinaryExpr + focalPredicates.Add((CoPredicate)fce.Function); + } + } } } else { // compute the preconditions of the prefix lemma @@ -1584,13 +1591,18 @@ namespace Microsoft.Dafny var subst = new FixpointLemmaSpecificationSubstituter(antecedents, new IdentifierExpr(k.tok, k.Name), this.reporter, false); var pre = subst.CloneExpr(p.E); prefixLemma.Req.Add(new MaybeFreeExpression(pre, p.IsFree)); + foreach (var e in antecedents) { + var fce = (FunctionCallExpr)e; // we expect "antecedents" to contain only FunctionCallExpr's + focalPredicates.Add((InductivePredicate)fce.Function); + } } } + reporter.Info(MessageSource.Resolver, com.tok, string.Format("{0} specialized for {1}", com.PrefixLemma.Name, Util.Comma(focalPredicates, p => p.Name))); // Compute the statement body of the prefix lemma Contract.Assume(prefixLemma.Body == null); // this is not supposed to have been filled in before if (com.Body != null) { var kMinusOne = new BinaryExpr(com.tok, BinaryExpr.Opcode.Sub, new IdentifierExpr(k.tok, k.Name), new LiteralExpr(com.tok, 1)); - var subst = new FixpointLemmaBodyCloner(com, kMinusOne, this.reporter); + var subst = new FixpointLemmaBodyCloner(com, kMinusOne, focalPredicates, this.reporter); var mainBody = subst.CloneBlockStmt(com.Body); var kPositive = new BinaryExpr(com.tok, BinaryExpr.Opcode.Lt, new LiteralExpr(com.tok, 0), new IdentifierExpr(k.tok, k.Name)); var condBody = new IfStmt(com.BodyStartTok, mainBody.EndTok, kPositive, mainBody, null); @@ -3571,7 +3583,7 @@ namespace Microsoft.Dafny var substituter = new Translator.AlphaConverting_Substituter(cs.Receiver, argsSubstMap, new Dictionary(), new Translator(resolver.reporter)); foreach (var ens in cs.Method.Ens) { var p = substituter.Substitute(ens.E); // substitute the call's actuals for the method's formals - resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ensures " + Printer.ExprToString(p) + ";"); + resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ensures " + Printer.ExprToString(p)); } } } diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy index d990ae51..0dce8af9 100644 --- a/Test/dafny0/CoinductiveProofs.dfy +++ b/Test/dafny0/CoinductiveProofs.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" /rewriteFocalPredicates:1 "%s" > "%t" // RUN: %diff "%s.expect" "%t" codatatype Stream = Cons(head: T, tail: Stream) @@ -12,6 +12,7 @@ copredicate Pos(s: Stream) { 0 < s.head && Pos(s.tail) } +predicate FullPos(s: Stream) { Pos(s) } // a way in the test file to sidestep focal-predicate rewrites colemma {:induction false} PosLemma0(n: int) requires 1 <= n; @@ -26,7 +27,25 @@ colemma {:induction false} PosLemma1(n: int) { PosLemma1(n + 1); if (*) { - assert Pos(Upward(n + 1)); // error: cannot conclude this here, because we only have prefix predicates + assert FullPos(Upward(n + 1)); // error: cannot conclude this here, because we only have prefix predicates + } +} + +colemma {:induction false} PosLemma2(n: int) + requires 1 <= n; + ensures Pos(Upward(n)); +{ + PosLemma2(n + 1); + if (*) { + assert Pos(Upward(n + 1)); // Pos gets rewritten to Pos#[_k-1], which does hold + } else if (*) { + assert Pos#[_k-1](Upward(n + 1)); // explicitly saying Pos#[_k-1] also holds + } else if (*) { + assert Pos#[_k](Upward(n + 1)); // error: this is not known to hold for _k and n+1 + } else if (*) { + assert Pos#[_k](Upward(n)); // but it does hold with Pos#[_k] and n (which is the postcondition of the prefix lemma) + } else if (*) { + assert Pos#[_k+1](Upward(n)); // error: this is too much to ask for } } @@ -65,13 +84,29 @@ colemma {:induction false} AlwaysLemma_X1(s: Stream) { AlwaysLemma_X1(s); // this is the right proof } +predicate FullX(s: Stream) { X(s) } // a way in the test file to sidestep focal-predicate rewrites colemma {:induction false} AlwaysLemma_X2(s: Stream) ensures X(s); { AlwaysLemma_X2(s); if (*) { - assert X(s); // error: cannot conclude the full predicate here + assert FullX(s); // error: cannot conclude the full predicate here + } +} + +colemma {:induction false} AlwaysLemma_X3(s: Stream) + ensures X(s); +{ + AlwaysLemma_X3(s); + if (*) { + assert X(s); // holds, because it gets rewritten to X#[_k-1] + } else if (*) { + assert X#[_k-1](s); // explicitly saying X#[_k-1] also holds + } else if (*) { + assert X#[_k](s); // in fact, X#[_k] holds, too (which is the postcondition of the prefix lemma) + } else if (*) { + assert X#[_k+1](s); // as it turns out, this holds too, since the definition of X makes X#[_k+1] equal X#[_k] } } @@ -79,6 +114,7 @@ copredicate Y(s: Stream) // this is equivalent to always returning 'true' { Y(s.tail) } +predicate FullY(s: Stream) { Y(s) } // a way in the test file to sidestep focal-predicate rewrites colemma {:induction false} AlwaysLemma_Y0(s: Stream) ensures Y(s); // prove that Y(s) really is always 'true' @@ -97,7 +133,24 @@ colemma {:induction false} AlwaysLemma_Y2(s: Stream) { AlwaysLemma_Y2(s.tail); if (*) { - assert Y(s.tail); // error: not provable here + assert FullY(s.tail); // error: not provable here + } +} + +colemma {:induction false} AlwaysLemma_Y3(s: Stream) + ensures Y(s); +{ + AlwaysLemma_Y3(s.tail); + if (*) { + assert Y(s.tail); // this holds, because it's rewritten to Y#[_k-1] + } else if (*) { + assert Y#[_k-1](s.tail); + } else if (*) { + assert Y#[_k](s.tail); // error: not known to hold for _k and s.tail + } else if (*) { + assert Y#[_k](s); // this is also the postcondition of the prefix lemma + } else if (*) { + assert Y#[_k+1](s); // error: this is too much to ask for } } diff --git a/Test/dafny0/CoinductiveProofs.dfy.expect b/Test/dafny0/CoinductiveProofs.dfy.expect index 2a5a2b0b..c4f4c405 100644 --- a/Test/dafny0/CoinductiveProofs.dfy.expect +++ b/Test/dafny0/CoinductiveProofs.dfy.expect @@ -1,50 +1,77 @@ -CoinductiveProofs.dfy(29,11): Error: assertion violation +CoinductiveProofs.dfy(30,11): Error: assertion violation +CoinductiveProofs.dfy(15,36): Related location CoinductiveProofs.dfy(13,16): Related location Execution trace: (0,0): anon0 (0,0): anon5_Then (0,0): anon6_Then -CoinductiveProofs.dfy(59,0): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(58,10): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(54,2): Related location +CoinductiveProofs.dfy(44,11): Error: assertion violation +CoinductiveProofs.dfy(13,16): Related location +Execution trace: + (0,0): anon0 + (0,0): anon13_Then + (0,0): anon16_Then +CoinductiveProofs.dfy(48,11): Error: assertion violation +CoinductiveProofs.dfy(13,16): Related location +Execution trace: + (0,0): anon0 + (0,0): anon13_Then + (0,0): anon18_Then +CoinductiveProofs.dfy(78,0): Error BP5003: A postcondition might not hold on this return path. +CoinductiveProofs.dfy(77,10): Related location: This is the postcondition that might not hold. +CoinductiveProofs.dfy(73,2): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -CoinductiveProofs.dfy(74,11): Error: assertion violation -CoinductiveProofs.dfy(54,2): Related location +CoinductiveProofs.dfy(94,11): Error: assertion violation +CoinductiveProofs.dfy(87,29): Related location +CoinductiveProofs.dfy(73,2): Related location Execution trace: (0,0): anon0 (0,0): anon5_Then (0,0): anon6_Then -CoinductiveProofs.dfy(91,0): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(90,10): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(80,2): Related location +CoinductiveProofs.dfy(127,0): Error BP5003: A postcondition might not hold on this return path. +CoinductiveProofs.dfy(126,10): Related location: This is the postcondition that might not hold. +CoinductiveProofs.dfy(115,2): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -CoinductiveProofs.dfy(100,11): Error: assertion violation -CoinductiveProofs.dfy(80,2): Related location +CoinductiveProofs.dfy(136,11): Error: assertion violation +CoinductiveProofs.dfy(117,29): Related location +CoinductiveProofs.dfy(115,2): Related location Execution trace: (0,0): anon0 (0,0): anon5_Then (0,0): anon6_Then -CoinductiveProofs.dfy(111,0): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(110,10): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(106,2): Related location +CoinductiveProofs.dfy(149,11): Error: assertion violation +CoinductiveProofs.dfy(115,2): Related location +Execution trace: + (0,0): anon0 + (0,0): anon13_Then + (0,0): anon16_Then +CoinductiveProofs.dfy(153,11): Error: assertion violation +CoinductiveProofs.dfy(115,2): Related location +Execution trace: + (0,0): anon0 + (0,0): anon13_Then + (0,0): anon18_Then +CoinductiveProofs.dfy(164,0): Error BP5003: A postcondition might not hold on this return path. +CoinductiveProofs.dfy(163,10): Related location: This is the postcondition that might not hold. +CoinductiveProofs.dfy(159,2): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -CoinductiveProofs.dfy(150,0): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(149,21): Related location: This is the postcondition that might not hold. +CoinductiveProofs.dfy(203,0): Error BP5003: A postcondition might not hold on this return path. +CoinductiveProofs.dfy(202,21): Related location: This is the postcondition that might not hold. CoinductiveProofs.dfy(4,23): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -CoinductiveProofs.dfy(156,0): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(155,21): Related location: This is the postcondition that might not hold. +CoinductiveProofs.dfy(209,0): Error BP5003: A postcondition might not hold on this return path. +CoinductiveProofs.dfy(208,21): Related location: This is the postcondition that might not hold. CoinductiveProofs.dfy(4,23): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -Dafny program verifier finished with 35 verified, 8 errors +Dafny program verifier finished with 42 verified, 12 errors diff --git a/Test/wishlist/tooltips-on-inductive-lemmas.dfy b/Test/wishlist/tooltips-on-inductive-lemmas.dfy deleted file mode 100644 index 1bd25437..00000000 --- a/Test/wishlist/tooltips-on-inductive-lemmas.dfy +++ /dev/null @@ -1,12 +0,0 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -inductive lemma P() - requires Q() { // WISH the tooltip for this was broken at some point between - // revisions 94ee216fe0cd (1179) and bd779dda3b3d (1785) - P(); -} - -inductive predicate Q() { - Q() -} diff --git a/Test/wishlist/tooltips-on-inductive-lemmas.dfy.expect b/Test/wishlist/tooltips-on-inductive-lemmas.dfy.expect deleted file mode 100644 index 4d036eef..00000000 --- a/Test/wishlist/tooltips-on-inductive-lemmas.dfy.expect +++ /dev/null @@ -1,7 +0,0 @@ -tooltips-on-inductive-lemmas.dfy(5,11): Info: Q -tooltips-on-inductive-lemmas.dfy(7,2): Info: P -tooltips-on-inductive-lemmas.dfy(11,2): Info: Q#[_k - 1] -tooltips-on-inductive-lemmas.dfy(4,16): Info: P# {:induction _k} -tooltips-on-inductive-lemmas.dfy(4,16): Info: P# decreases _k - -Dafny program verifier finished with 3 verified, 0 errors -- cgit v1.2.3