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/dafny2/SnapshotableTrees.dfy.expect | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Test/dafny2/SnapshotableTrees.dfy.expect') diff --git a/Test/dafny2/SnapshotableTrees.dfy.expect b/Test/dafny2/SnapshotableTrees.dfy.expect index 849b9e38..808fe0f9 100644 --- a/Test/dafny2/SnapshotableTrees.dfy.expect +++ b/Test/dafny2/SnapshotableTrees.dfy.expect @@ -1,5 +1,5 @@ -SnapshotableTrees.dfy(68,24): Error BP5002: A precondition for this call might not hold. -SnapshotableTrees.dfy(648,16): Related location: This is the precondition that might not hold. +SnapshotableTrees.dfy(68,23): Error BP5002: A precondition for this call might not hold. +SnapshotableTrees.dfy(648,15): Related location: This is the precondition that might not hold. Execution trace: (0,0): anon0 (0,0): anon3_Then -- cgit v1.2.3 From 736969063f99babb854a2ac7c2c2b0d11a8fc253 Mon Sep 17 00:00:00 2001 From: leino Date: Sat, 24 Oct 2015 17:43:46 -0700 Subject: In method and iterator specifications, inline top-level predicates (except protected predicated in cross-module calls) like in other places. --- Source/Dafny/Translator.cs | 166 +++++++++++---------- Test/dafny0/TriggerInPredicate.dfy.expect | 1 + Test/dafny2/SnapshotableTrees.dfy.expect | 9 +- .../triggers-prevent-some-inlining.dfy.expect | 2 + 4 files changed, 98 insertions(+), 80 deletions(-) (limited to 'Test/dafny2/SnapshotableTrees.dfy.expect') diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 7d3f570d..172005cc 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1466,13 +1466,15 @@ namespace Microsoft.Dafny { /// /// Returns true if the body of function "f" is available in module "context". - /// This happens when "f" has a body, "f" is not opaque, and either "f" is declared - /// in module "context" or "f" is not protected. + /// This happens when the following conditions all hold: + /// - "f" has a body + /// - "f" is not opaque + /// - "f" is declared as protected, then "context" is the current module and parameter "revealProtectedBody" is passed in as "true". /// - static bool FunctionBodyIsAvailable(Function f, ModuleDefinition context) { + static bool FunctionBodyIsAvailable(Function f, ModuleDefinition context, bool revealProtectedBody) { Contract.Requires(f != null); Contract.Requires(context != null); - return f.Body != null && !IsOpaqueFunction(f) && (f.EnclosingClass.Module == context || !f.IsProtected); + return f.Body != null && !IsOpaqueFunction(f) && (!f.IsProtected || (revealProtectedBody && f.EnclosingClass.Module == context)); } static bool IsOpaqueFunction(Function f) { Contract.Requires(f != null); @@ -1571,8 +1573,7 @@ namespace Microsoft.Dafny { req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment)); comment = null; } else { - bool splitHappened; // we actually don't care - foreach (var s in TrSplitExpr(p.E, etran, kind == MethodTranslationKind.InterModuleCall ? 0 : int.MaxValue, true, out splitHappened)) { + foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) { if (kind == MethodTranslationKind.IntraModuleCall && RefinementToken.IsInherited(s.E.tok, currentModule)) { // this precondition was inherited into this module, so just ignore it } else { @@ -1589,8 +1590,7 @@ namespace Microsoft.Dafny { ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment)); comment = null; } else { - bool splitHappened; // we actually don't care - foreach (var s in TrSplitExpr(p.E, etran, kind == MethodTranslationKind.InterModuleCall ? 0 : int.MaxValue, true, out splitHappened)) { + foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) { if (kind == MethodTranslationKind.Implementation && RefinementToken.IsInherited(s.E.tok, currentModule)) { // this postcondition was inherited into this module, so just ignore it } else { @@ -2966,7 +2966,7 @@ namespace Microsoft.Dafny { { var functionHeight = currentModule.CallGraph.GetSCCRepresentativeId(f); var splits = new List(); - bool splitHappened/*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight,false, etran); + bool splitHappened/*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight, true, false, etran); foreach (var s in splits) { if (s.IsChecked && !RefinementToken.IsInherited(s.E.tok, currentModule)) @@ -3975,7 +3975,7 @@ namespace Microsoft.Dafny { foreach (Expression p in f.Ens) { var functionHeight = currentModule.CallGraph.GetSCCRepresentativeId(f); var splits = new List(); - bool splitHappened /*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight, true, etran); + bool splitHappened /*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight, true, true, etran); foreach (var s in splits) { if (s.IsChecked && !RefinementToken.IsInherited(s.E.tok, currentModule)) { ens.Add(Ensures(s.E.tok, false, s.E, null, null)); @@ -6233,8 +6233,7 @@ namespace Microsoft.Dafny { req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment)); comment = null; } else { - bool splitHappened; // we actually don't care - foreach (var s in TrSplitExpr(p.E, etran, kind == MethodTranslationKind.InterModuleCall ? 0 : int.MaxValue, true /* kind == MethodTranslationKind.Implementation */, out splitHappened)) { + foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) { if (s.IsOnlyChecked && bodyKind) { // don't include in split } else if (s.IsOnlyFree && !bodyKind) { @@ -6254,8 +6253,7 @@ namespace Microsoft.Dafny { if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) { ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, null)); } else { - bool splitHappened; // we actually don't care - foreach (var s in TrSplitExpr(p.E, etran, kind == MethodTranslationKind.InterModuleCall ? 0 : int.MaxValue, true /* kind == MethodTranslationKind.Implementation */ , out splitHappened)) { + foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) { var post = s.E; if (kind == MethodTranslationKind.Implementation && RefinementToken.IsInherited(s.E.tok, currentModule)) { // this postcondition was inherited into this module, so make it into the form "$_reverifyPost ==> s.E" @@ -11115,7 +11113,7 @@ namespace Microsoft.Dafny { result = translator.CondApplyUnbox(e.tok, result, e.Function.ResultType, e.Type); bool callIsLit = argsAreLit - && Translator.FunctionBodyIsAvailable(e.Function, translator.currentModule) + && Translator.FunctionBodyIsAvailable(e.Function, translator.currentModule, true) && !e.Function.Reads.Any(); // Function could depend on external values if (callIsLit) { result = MaybeLit(result, ty); @@ -12754,18 +12752,20 @@ namespace Microsoft.Dafny { Contract.Ensures(Contract.Result>() != null); var splits = new List(); - splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, apply_induction, etran); + splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, true, apply_induction, etran); return splits; } - List/*!*/ TrSplitExpr(Expression expr, ExpressionTranslator etran, int heightLimit, bool apply_induction, out bool splitHappened) + List TrSplitExprForMethodSpec(Expression expr, ExpressionTranslator etran, MethodTranslationKind kind) { Contract.Requires(expr != null); Contract.Requires(etran != null); Contract.Ensures(Contract.Result>() != null); var splits = new List(); - splitHappened = TrSplitExpr(expr, splits, true, heightLimit, apply_induction, etran); + var apply_induction = true;/*kind == MethodTranslationKind.Implementation*/; + bool splitHappened; // we don't actually care + splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, kind != MethodTranslationKind.InterModuleCall, apply_induction, etran); return splits; } @@ -12795,7 +12795,7 @@ namespace Microsoft.Dafny { /// if its body is available in the current context and its height is less than "heightLimit" (if "heightLimit" is /// passed in as 0, then no functions will be inlined). /// - bool TrSplitExpr(Expression expr, List/*!*/ splits, bool position, int heightLimit, bool apply_induction, ExpressionTranslator etran) { + bool TrSplitExpr(Expression expr, List/*!*/ splits, bool position, int heightLimit, bool inlineProtectedFunctions, bool apply_induction, ExpressionTranslator etran) { Contract.Requires(expr != null); Contract.Requires(expr.Type.IsBoolType || (expr is BoxingCastExpr && ((BoxingCastExpr)expr).E.Type.IsBoolType)); Contract.Requires(splits != null); @@ -12804,7 +12804,7 @@ namespace Microsoft.Dafny { if (expr is BoxingCastExpr) { var bce = (BoxingCastExpr)expr; var ss = new List(); - if (TrSplitExpr(bce.E, ss, position, heightLimit, apply_induction, etran)) { + if (TrSplitExpr(bce.E, ss, position, heightLimit, inlineProtectedFunctions, apply_induction, etran)) { foreach (var s in ss) { splits.Add(new SplitExprInfo(s.Kind, CondApplyBox(s.E.tok, s.E, bce.FromType, bce.ToType))); } @@ -12813,22 +12813,22 @@ namespace Microsoft.Dafny { } else if (expr is ConcreteSyntaxExpression) { var e = (ConcreteSyntaxExpression)expr; - return TrSplitExpr(e.ResolvedExpression, splits, position, heightLimit, apply_induction, etran); + return TrSplitExpr(e.ResolvedExpression, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); } else if (expr is LetExpr) { var e = (LetExpr)expr; if (e.Exact) { - return TrSplitExpr(etran.GetSubstitutedBody(e), splits, position, heightLimit, apply_induction, etran); + return TrSplitExpr(etran.GetSubstitutedBody(e), splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); } else { var d = LetDesugaring(e); - return TrSplitExpr(d, splits, position, heightLimit, apply_induction, etran); + return TrSplitExpr(d, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); } } else if (expr is UnaryOpExpr) { var e = (UnaryOpExpr)expr; if (e.Op == UnaryOpExpr.Opcode.Not) { var ss = new List(); - if (TrSplitExpr(e.E, ss, !position, heightLimit, apply_induction, etran)) { + if (TrSplitExpr(e.E, ss, !position, heightLimit, inlineProtectedFunctions, apply_induction, etran)) { foreach (var s in ss) { splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Unary(s.E.tok, UnaryOperator.Opcode.Not, s.E))); } @@ -12839,13 +12839,13 @@ namespace Microsoft.Dafny { } else if (expr is BinaryExpr) { var bin = (BinaryExpr)expr; if (position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) { - TrSplitExpr(bin.E0, splits, position, heightLimit, apply_induction, etran); - TrSplitExpr(bin.E1, splits, position, heightLimit, apply_induction, etran); + TrSplitExpr(bin.E0, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); + TrSplitExpr(bin.E1, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); return true; } else if (!position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Or) { - TrSplitExpr(bin.E0, splits, position, heightLimit, apply_induction, etran); - TrSplitExpr(bin.E1, splits, position, heightLimit, apply_induction, etran); + TrSplitExpr(bin.E0, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); + TrSplitExpr(bin.E1, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); return true; } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) { @@ -12853,14 +12853,14 @@ namespace Microsoft.Dafny { if (position) { var lhs = etran.TrExpr(bin.E0); var ss = new List(); - TrSplitExpr(bin.E1, ss, position, heightLimit, apply_induction, etran); + TrSplitExpr(bin.E1, ss, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); foreach (var s in ss) { // as the source location in the following implication, use that of the translated "s" splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, lhs, s.E))); } } else { var ss = new List(); - TrSplitExpr(bin.E0, ss, !position, heightLimit, apply_induction, etran); + TrSplitExpr(bin.E0, ss, !position, heightLimit, inlineProtectedFunctions, apply_induction, etran); var rhs = etran.TrExpr(bin.E1); foreach (var s in ss) { // as the source location in the following implication, use that of the translated "s" @@ -12907,8 +12907,8 @@ namespace Microsoft.Dafny { var ssThen = new List(); var ssElse = new List(); - TrSplitExpr(ite.Thn, ssThen, position, heightLimit, apply_induction, etran); - TrSplitExpr(ite.Els, ssElse, position, heightLimit, apply_induction, etran); + TrSplitExpr(ite.Thn, ssThen, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); + TrSplitExpr(ite.Els, ssElse, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); var op = position ? BinaryOperator.Opcode.Imp : BinaryOperator.Opcode.And; var test = etran.TrExpr(ite.Test); @@ -12934,14 +12934,14 @@ namespace Microsoft.Dafny { if (position) { var conclusion = etran.TrExpr(e.GetSConclusion()); var ss = new List(); - TrSplitExpr(e.E, ss, position, heightLimit, apply_induction, etran); + TrSplitExpr(e.E, ss, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); foreach (var s in ss) { // as the source location in the following implication, use that of the translated "s" splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, conclusion, s.E))); } } else { var ss = new List(); - TrSplitExpr(e.GetSConclusion(), ss, !position, heightLimit, apply_induction, etran); + TrSplitExpr(e.GetSConclusion(), ss, !position, heightLimit, inlineProtectedFunctions, apply_induction, etran); var rhs = etran.TrExpr(e.E); foreach (var s in ss) { // as the source location in the following implication, use that of the translated "s" @@ -12952,7 +12952,7 @@ namespace Microsoft.Dafny { } else if (expr is OldExpr) { var e = (OldExpr)expr; - return TrSplitExpr(e.E, splits, position, heightLimit, apply_induction, etran.Old); + return TrSplitExpr(e.E, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran.Old); } else if (expr is FunctionCallExpr && position) { var fexp = (FunctionCallExpr)expr; @@ -12961,22 +12961,17 @@ namespace Microsoft.Dafny { var module = f.EnclosingClass.Module; var functionHeight = module.CallGraph.GetSCCRepresentativeId(f); - if (module == currentModule && functionHeight < heightLimit && f.Body != null && !(f.Body.Resolved is MatchExpr)) { + if (functionHeight < heightLimit && f.Body != null && !(f.Body.Resolved is MatchExpr)) { if (RefinementToken.IsInherited(fexp.tok, currentModule) && f is Predicate && ((Predicate)f).BodyOrigin == Predicate.BodyOriginKind.DelayedDefinition && (codeContext == null || !codeContext.MustReverify)) { // The function was inherited as body-less but is now given a body. Don't inline the body (since, apparently, everything // that needed to be proved about the function was proved already in the previous module, even without the body definition). - } else if (!FunctionBodyIsAvailable(f, currentModule)) { + } else if (!FunctionBodyIsAvailable(f, currentModule, inlineProtectedFunctions)) { // Don't inline opaque functions or foreign protected functions } else if (Attributes.Contains(f.Attributes, "no_inline")) { // User manually prevented inlining - } else if (CanSafelyInline(fexp, f)) { - // inline this body - var body = GetSubstitutedBody(fexp, f, false); - var typeSpecializedBody = GetSubstitutedBody(fexp, f, true); - var typeSpecializedResultType = Resolver.SubstType(f.ResultType, fexp.TypeArgumentSubstitutions); - + } else { // Produce, for a "body" split into b0, b1, b2: // checked F#canCall(args) ==> F(args) || b0 // checked F#canCall(args) ==> F(args) || b1 @@ -12999,49 +12994,62 @@ namespace Microsoft.Dafny { // F(args) fargs = etran.TrExpr(fexp); - // recurse on body - var ss = new List(); - TrSplitExpr(typeSpecializedBody, ss, position, functionHeight, apply_induction, etran); - var needsTokenAdjust = TrSplitNeedsTokenAdjustment(typeSpecializedBody); - foreach (var s in ss) { - if (s.IsChecked) { - var unboxedConjunct = CondApplyUnbox(s.E.tok, s.E, typeSpecializedResultType, expr.Type); - var bodyOrConjunct = Bpl.Expr.Or(fargs, unboxedConjunct); - var tok = needsTokenAdjust ? (IToken)new ForceCheckToken(typeSpecializedBody.tok) : (IToken)new NestedToken(fexp.tok, s.E.tok); - var p = Bpl.Expr.Binary(tok, BinaryOperator.Opcode.Imp, canCall, bodyOrConjunct); - splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p)); + if (!CanSafelyInline(fexp, f)) { + // Skip inlining, as it would cause arbitrary expressions to pop up in the trigger + // TODO this should appear at the outmost call site, not at the innermost. See SnapshotableTrees.dfy + reporter.Info(MessageSource.Translator, fexp.tok, "Some instances of this call cannot safely be inlined."); + // F#canCall(args) ==> F(args) + var p = Bpl.Expr.Binary(fargs.tok, BinaryOperator.Opcode.Imp, canCall, fargs); + splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p)); + // F#canCall(args) && F(args) + var fr = Bpl.Expr.And(canCall, fargs); + splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, fr)); + + } else { + // inline this body + var typeSpecializedBody = GetSubstitutedBody(fexp, f); + var typeSpecializedResultType = Resolver.SubstType(f.ResultType, fexp.TypeArgumentSubstitutions); + + // recurse on body + var ss = new List(); + TrSplitExpr(typeSpecializedBody, ss, position, functionHeight, inlineProtectedFunctions, apply_induction, etran); + var needsTokenAdjust = TrSplitNeedsTokenAdjustment(typeSpecializedBody); + foreach (var s in ss) { + if (s.IsChecked) { + var unboxedConjunct = CondApplyUnbox(s.E.tok, s.E, typeSpecializedResultType, expr.Type); + var bodyOrConjunct = Bpl.Expr.Or(fargs, unboxedConjunct); + var tok = needsTokenAdjust ? (IToken)new ForceCheckToken(typeSpecializedBody.tok) : (IToken)new NestedToken(fexp.tok, s.E.tok); + var p = Bpl.Expr.Binary(tok, BinaryOperator.Opcode.Imp, canCall, bodyOrConjunct); + splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p)); + } } - } - // allocatedness for arguments to the inlined call in body - if (typeSpecializedBody is FunctionCallExpr) { - FunctionCallExpr e = (FunctionCallExpr)typeSpecializedBody; - for (int i = 0; i < e.Args.Count; i++) { - Expression ee = e.Args[i]; - Type t = e.Function.Formals[i].Type; - Expr tr_ee = etran.TrExpr(ee); - Bpl.Expr wh = GetWhereClause(e.tok, tr_ee, cce.NonNull(ee.Type), etran); - if (wh != null) { fargs = Bpl.Expr.And(fargs, wh); } + // allocatedness for arguments to the inlined call in body + if (typeSpecializedBody is FunctionCallExpr) { + FunctionCallExpr e = (FunctionCallExpr)typeSpecializedBody; + for (int i = 0; i < e.Args.Count; i++) { + Expression ee = e.Args[i]; + Type t = e.Function.Formals[i].Type; + Expr tr_ee = etran.TrExpr(ee); + Bpl.Expr wh = GetWhereClause(e.tok, tr_ee, cce.NonNull(ee.Type), etran); + if (wh != null) { fargs = Bpl.Expr.And(fargs, wh); } + } } - } - // body - var trBody = etran.TrExpr(typeSpecializedBody); - trBody = CondApplyUnbox(trBody.tok, trBody, typeSpecializedResultType, expr.Type); - // F#canCall(args) && F(args) && (b0 && b1 && b2) - var fr = Bpl.Expr.And(canCall, BplAnd(fargs, trBody)); - splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, fr)); + // body + var trBody = etran.TrExpr(typeSpecializedBody); + trBody = CondApplyUnbox(trBody.tok, trBody, typeSpecializedResultType, expr.Type); + // F#canCall(args) && F(args) && (b0 && b1 && b2) + var fr = Bpl.Expr.And(canCall, BplAnd(fargs, trBody)); + splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, fr)); + } return true; - } else { - // Skip inlining, as it would cause arbitrary expressions to pop up in the trigger - // TODO this should appear at the outmost call site, not at the innermost. See SnapshotableTrees.dfy - reporter.Info(MessageSource.Translator, fexp.tok, "Some instances of this call cannot safely be inlined."); } } } else if (expr is QuantifierExpr && ((QuantifierExpr)expr).SplitQuantifier != null) { - return TrSplitExpr(((QuantifierExpr)expr).SplitQuantifierExpression, splits, position, heightLimit, apply_induction, etran); + return TrSplitExpr(((QuantifierExpr)expr).SplitQuantifierExpression, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); } else if (((position && expr is ForallExpr) || (!position && expr is ExistsExpr)) /* NB: only for type arg less quantifiers for now: */ && ((QuantifierExpr)expr).TypeArgs.Count == 0) { @@ -13220,14 +13228,14 @@ namespace Microsoft.Dafny { } } - private Expression GetSubstitutedBody(FunctionCallExpr fexp, Function f, bool specializeTypeParameters) { + private Expression GetSubstitutedBody(FunctionCallExpr fexp, Function f) { Contract.Requires(fexp != null); Contract.Requires(f != null); var substMap = new Dictionary(); Contract.Assert(fexp.Args.Count == f.Formals.Count); for (int i = 0; i < f.Formals.Count; i++) { Formal p = f.Formals[i]; - var formalType = specializeTypeParameters ? Resolver.SubstType(p.Type, fexp.TypeArgumentSubstitutions) : p.Type; + var formalType = Resolver.SubstType(p.Type, fexp.TypeArgumentSubstitutions); Expression arg = fexp.Args[i]; arg = new BoxingCastExpr(arg, cce.NonNull(arg.Type), formalType); arg.Type = formalType; // resolve here @@ -13238,7 +13246,7 @@ namespace Microsoft.Dafny { var pp = (PrefixPredicate)f; body = PrefixSubstitution(pp, body); } - body = Substitute(body, fexp.Receiver, substMap, specializeTypeParameters ? fexp.TypeArgumentSubstitutions : null); + body = Substitute(body, fexp.Receiver, substMap, fexp.TypeArgumentSubstitutions); return body; } diff --git a/Test/dafny0/TriggerInPredicate.dfy.expect b/Test/dafny0/TriggerInPredicate.dfy.expect index b3fb9cc0..b3d4ff34 100644 --- a/Test/dafny0/TriggerInPredicate.dfy.expect +++ b/Test/dafny0/TriggerInPredicate.dfy.expect @@ -2,5 +2,6 @@ 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. +TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined. Dafny program verifier finished with 8 verified, 0 errors diff --git a/Test/dafny2/SnapshotableTrees.dfy.expect b/Test/dafny2/SnapshotableTrees.dfy.expect index 808fe0f9..68b4ff73 100644 --- a/Test/dafny2/SnapshotableTrees.dfy.expect +++ b/Test/dafny2/SnapshotableTrees.dfy.expect @@ -1,8 +1,15 @@ SnapshotableTrees.dfy(68,23): Error BP5002: A precondition for this call might not hold. SnapshotableTrees.dfy(648,15): Related location: This is the precondition that might not hold. +SnapshotableTrees.dfy(545,15): Related location +Execution trace: + (0,0): anon0 + (0,0): anon3_Then +SnapshotableTrees.dfy(68,23): Error BP5002: A precondition for this call might not hold. +SnapshotableTrees.dfy(648,15): Related location: This is the precondition that might not hold. +SnapshotableTrees.dfy(548,18): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -Dafny program verifier finished with 65 verified, 1 error +Dafny program verifier finished with 65 verified, 2 errors Compiled assembly into SnapshotableTrees.exe diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy.expect b/Test/triggers/triggers-prevent-some-inlining.dfy.expect index 4c24893e..0b6f3e30 100644 --- a/Test/triggers/triggers-prevent-some-inlining.dfy.expect +++ b/Test/triggers/triggers-prevent-some-inlining.dfy.expect @@ -3,5 +3,7 @@ triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call can triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call cannot safely be inlined. triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call cannot safely be inlined. triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call cannot safely be inlined. +triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call cannot safely be inlined. +triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call cannot safely be inlined. Dafny program verifier finished with 4 verified, 0 errors -- cgit v1.2.3