Include conditions from code in related location error messages

Source/DafnyCore/DafnyConsolePrinter.cs

@@ -89,7 +89,7 @@ public override void ReportBplError(Boogie.IToken tok, string message, bool erro
       message = $"{category}: {message}";
     }
 
-    var dafnyToken = BoogieGenerator.ToDafnyToken(options.Get(Snippets.ShowSnippets), tok);
+    var dafnyToken = BoogieGenerator.ToDafnyToken(tok);
     message = $"{dafnyToken.TokenToString(Options)}: {message}";
 
     if (error) {

Source/DafnyCore/Generic/ReporterExtensions.cs

@@ -14,13 +14,13 @@ public static void ReportBoogieError(this ErrorReporter reporter, ErrorInformati
       if (auxiliaryInformation.Category == RelatedMessageCategory || auxiliaryInformation.Category == AssertedExprCategory) {
         error.Msg += "\n" + auxiliaryInformation.FullMsg;
       } else if (auxiliaryInformation.Category == RelatedLocationCategory) {
-        relatedInformation.AddRange(CreateDiagnosticRelatedInformationFor(BoogieGenerator.ToDafnyToken(true, auxiliaryInformation.Tok), auxiliaryInformation.Msg, usingSnippets));
+        relatedInformation.AddRange(CreateDiagnosticRelatedInformationFor(BoogieGenerator.ToDafnyToken(auxiliaryInformation.Tok), auxiliaryInformation.Msg, usingSnippets));
       } else {
         // The execution trace is an additional auxiliary which identifies itself with
         // line=0 and character=0. These positions cause errors when exposing them, Furthermore,
         // the execution trace message appears to not have any interesting information.
         if (auxiliaryInformation.Tok.line > 0) {
-          reporter.Info(MessageSource.Verifier, BoogieGenerator.ToDafnyToken(true, auxiliaryInformation.Tok), auxiliaryInformation.Msg);
+          reporter.Info(MessageSource.Verifier, BoogieGenerator.ToDafnyToken(auxiliaryInformation.Tok), auxiliaryInformation.Msg);
         }
       }
     }
@@ -33,7 +33,7 @@ public static void ReportBoogieError(this ErrorReporter reporter, ErrorInformati
       relatedInformation.AddRange(CreateDiagnosticRelatedInformationFor(innerToken, msg, usingSnippets));
     }
 
-    var dafnyToken = BoogieGenerator.ToDafnyToken(useRange, error.Tok);
+    var dafnyToken = BoogieGenerator.ToDafnyToken(error.Tok);
 
     var tokens = new[] { dafnyToken }.Concat(relatedInformation.Select(i => i.Token)).ToList();
     IOrigin previous = tokens.Last();
@@ -48,25 +48,20 @@ public static void ReportBoogieError(this ErrorReporter reporter, ErrorInformati
   private const string RelatedMessageCategory = "Related message";
   public const string AssertedExprCategory = "Asserted expression";
   public static readonly string PostConditionFailingMessage = new EnsuresDescription(null, null, null).FailureDescription;
-  private static string FormatRelated(string related) {
-    return $"Could not prove: {related}";
-  }
 
   public static IEnumerable<DafnyRelatedInformation> CreateDiagnosticRelatedInformationFor(IOrigin token, string? message, bool usingSnippets) {
     var (tokenForMessage, inner, newMessage) = token is NestedOrigin nestedToken ? (nestedToken.Outer, nestedToken.Inner, nestedToken.Message) : (token, null, null);
-    var dafnyToken = BoogieGenerator.ToDafnyToken(true, tokenForMessage);
+    var dafnyToken = BoogieGenerator.ToDafnyToken(tokenForMessage);
 
-    // Turning this on changes many regression tests, in a way that might be considered good,
-    // but it should be turned on in a separate PR
-    // There seem to be no LSP tests for this behavior, so turning it off did not affect those.
-    // if (!usingSnippets && dafnyToken.IncludesRange) {
-    //   if (message == PostConditionFailingMessage) {
-    //     var postcondition = dafnyToken.PrintOriginal();
-    //     message = $"this postcondition might not hold: {postcondition}";
-    //   } else if (message == null|| message == RelatedLocationMessage*/) {
-    //     message = FormatRelated(dafnyToken.PrintOriginal());
-    //   }
-    // }
+    if (!usingSnippets && dafnyToken.IncludesRange) {
+      if (message == PostConditionFailingMessage) {
+        var postcondition = dafnyToken.PrintOriginal();
+        message = $"this postcondition could not be proved: {postcondition}";
+      } else if (message == null || message == RelatedLocationMessage) {
+        string condition = dafnyToken.PrintOriginal();
+        message = $"could not prove: {condition}";
+      }
+    }
 
     message ??= "this proposition could not be proved";
 

Source/DafnyCore/JsonDiagnostics.cs

@@ -24,7 +24,7 @@ private static JsonObject SerializeRange(Boogie.IToken tok) {
     var range = new JsonObject {
       ["start"] = SerializePosition(tok),
     };
-    var origin = BoogieGenerator.ToDafnyToken(true, tok);
+    var origin = BoogieGenerator.ToDafnyToken(tok);
     if (origin.IncludesRange) {
       range["end"] = SerializePosition(origin.EndToken);
     }

Source/DafnyCore/Pipeline/BoogieExtensions.cs

@@ -61,7 +61,7 @@ public static Range GetLspRange(this Boogie.IToken token, bool nameRange = false
       if (token is NestedOrigin nestedToken) {
         return GetLspRange(nestedToken.Outer, nameRange);
       }
-      var dafnyToken = BoogieGenerator.ToDafnyToken(!nameRange, token);
+      var dafnyToken = BoogieGenerator.ToDafnyToken(token);
       return GetLspRangeGeneric(dafnyToken.StartToken, dafnyToken.EndToken);
     }
 

Source/DafnyCore/Pipeline/Compilation.cs

@@ -403,14 +403,14 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT
       return Enumerable.Empty<(IOrigin Group, List<IVerificationTask> Tasks)>();
     }
     var sortedTasks = ranges.OrderBy(r =>
-      BoogieGenerator.ToDafnyToken(true, r.Token).StartToken).ToList();
+      BoogieGenerator.ToDafnyToken(r.Token).StartToken).ToList();
     var groups = new List<(IOrigin Group, List<IVerificationTask> Tasks)>();
     var currentGroup = new List<IVerificationTask> { sortedTasks[0] };
-    var currentGroupRange = BoogieGenerator.ToDafnyToken(true, currentGroup[0].Token);
+    var currentGroupRange = BoogieGenerator.ToDafnyToken(currentGroup[0].Token);
 
     for (int i = 1; i < sortedTasks.Count; i++) {
       var currentTask = sortedTasks[i];
-      var currentTaskRange = BoogieGenerator.ToDafnyToken(true, currentTask.Token);
+      var currentTaskRange = BoogieGenerator.ToDafnyToken(currentTask.Token);
       bool overlapsWithGroup = currentGroupRange.Intersects(currentTaskRange);
 
       if (overlapsWithGroup) {
@@ -474,7 +474,7 @@ public async Task Cancel(FilePosition filePosition) {
   }
 
   private void HandleStatusUpdate(ICanVerify canVerify, IVerificationTask verificationTask, IVerificationStatus boogieStatus) {
-    var tokenString = BoogieGenerator.ToDafnyToken(true, verificationTask.Split.Token).TokenToString(Options);
+    var tokenString = BoogieGenerator.ToDafnyToken(verificationTask.Split.Token).TokenToString(Options);
     logger.LogDebug($"Received Boogie status {boogieStatus} for {tokenString}, version {Input.Version}");
 
     updates.OnNext(new BoogieUpdate(transformedProgram!.ProofDependencyManager, canVerify,
@@ -539,7 +539,7 @@ public static List<DafnyDiagnostic> GetDiagnosticsFromResult(DafnyOptions option
     List<DafnyDiagnostic> diagnostics = new();
     errorReporter.Updates.Subscribe(d => diagnostics.Add(d.Diagnostic));
 
-    ReportDiagnosticsInResult(options, canVerify.NavigationToken.val, BoogieGenerator.ToDafnyToken(true, task.Token),
+    ReportDiagnosticsInResult(options, canVerify.NavigationToken.val, BoogieGenerator.ToDafnyToken(task.Token),
       task.Split.Implementation.GetTimeLimit(options), result, errorReporter);
 
     return diagnostics.OrderBy(d => d.Token.GetLspPosition()).ToList();

Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs

@@ -894,13 +894,13 @@ static Bpl.Expr BplFormalVar(string name, Bpl.Type ty, bool incoming, List<Bpl.V
       return e;
     }
 
-    public static IOrigin ToDafnyToken(bool reportRanges, Bpl.IToken boogieToken) {
+    public static IOrigin ToDafnyToken(Bpl.IToken boogieToken) {
       if (boogieToken == null) {
         return null;
       } else if (boogieToken is IOrigin dafnyToken) {
         return dafnyToken;
       } else if (boogieToken is VCGeneration.TokenWrapper tokenWrapper) {
-        return ToDafnyToken(reportRanges, tokenWrapper.Inner);
+        return ToDafnyToken(tokenWrapper.Inner);
       } else if (ReferenceEquals(boogieToken, Boogie.Token.NoToken)) {
         return Token.NoToken;
       } else {

Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs

@@ -342,7 +342,7 @@ bool TrSplitExpr(BodyTranslationContext context, Expression expr, List<SplitExpr
                   foreach (var kase in InductionCases(n.Type, nn[i], etran)) {
                     foreach (var cs in caseProduct) {
                       if (kase != Bpl.Expr.True) {  // if there's no case, don't add anything to the token
-                        newCases.Add(Bpl.Expr.Binary(new NestedOrigin(ToDafnyToken(flags.ReportRanges, cs.tok), ToDafnyToken(flags.ReportRanges, kase.tok)), Bpl.BinaryOperator.Opcode.And, cs, kase));
+                        newCases.Add(Bpl.Expr.Binary(new NestedOrigin(ToDafnyToken(cs.tok), ToDafnyToken(kase.tok)), Bpl.BinaryOperator.Opcode.And, cs, kase));
                       } else {
                         newCases.Add(cs);
                       }
@@ -640,7 +640,7 @@ private Expression GetSubstitutedBody(FunctionCallExpr fexp, Function f) {
 
 
     SplitExprInfo ToSplitExprInfo(SplitExprInfo.K kind, Expr e) {
-      return new SplitExprInfo(flags.ReportRanges, kind, e);
+      return new SplitExprInfo(kind, e);
     }
 
     public class SplitExprInfo {
@@ -651,12 +651,11 @@ public enum K { Free, Checked, Both }
       public bool IsChecked { get { return Kind != K.Free; } }
       public readonly Expr E;
       public IOrigin Tok;
-      public SplitExprInfo(bool reportRanges, K kind, Expr e) {
+      public SplitExprInfo(K kind, Expr e) {
         Contract.Requires(e != null && e.tok != null);
-        // TODO:  Contract.Requires(kind == K.Free || e.Tok.IsValid);
         Kind = kind;
         E = e;
-        Tok = ToDafnyToken(reportRanges, e.tok);
+        Tok = ToDafnyToken(e.tok);
       }
     }
   }

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -70,7 +70,6 @@ public TranslatorFlags(DafnyOptions options) {
 
       public bool InsertChecksums { get; init; }
       public string UniqueIdPrefix = null;
-      public bool ReportRanges = false;
     }
 
     [NotDelayed]
@@ -80,9 +79,7 @@ public BoogieGenerator(ErrorReporter reporter, ProofDependencyManager depManager
       this.proofDependencies = depManager;
       this.reporter = reporter;
       if (flags == null) {
-        flags = new TranslatorFlags(options) {
-          ReportRanges = options.Get(Snippets.ShowSnippets)
-        };
+        flags = new TranslatorFlags(options);
       }
       this.flags = flags;
       Bpl.Program boogieProgram = ReadPrelude();
@@ -3493,9 +3490,9 @@ private void ReportAssertion(IOrigin tok, ProofObligationDescription description
       }
 
       if (options.Get(CommonOptionBag.ShowAssertions) > CommonOptionBag.AssertionShowMode.None && description.IsImplicit) {
-        reporter.Info(MessageSource.Translator, ToDafnyToken(false, tok), "Implicit assertion: " + description.ShortDescription, "isAssertion");
+        reporter.Info(MessageSource.Translator, ToDafnyToken(tok), "Implicit assertion: " + description.ShortDescription, "isAssertion");
       } else if (options.Get(CommonOptionBag.ShowAssertions) == CommonOptionBag.AssertionShowMode.All) {
-        reporter.Info(MessageSource.Translator, ToDafnyToken(false, tok), "Explicit assertion: " + description.ShortDescription, "isAssertion");
+        reporter.Info(MessageSource.Translator, ToDafnyToken(tok), "Explicit assertion: " + description.ShortDescription, "isAssertion");
       }
     }
 
@@ -4056,10 +4053,10 @@ internal class BoogieWrapper : Expression {
       public readonly Bpl.Expr Expr;
 
       public BoogieWrapper(Bpl.Expr expr, Type dafnyType)
-        : base(ToDafnyToken(false, expr.tok)) {
+        : base(ToDafnyToken(expr.tok)) {
         Contract.Requires(expr != null);
         Contract.Requires(dafnyType != null);
-        Origin = ToDafnyToken(true, expr.tok);
+        Origin = ToDafnyToken(expr.tok);
         Expr = expr;
         Type = dafnyType;  // resolve immediately
       }

Source/DafnyCore/Verifier/ProofDependency.cs

@@ -60,7 +60,7 @@ public class ProofObligationDependency : ProofDependency {
       $"{ProofObligation.SuccessDescription}";
 
   public ProofObligationDependency(Microsoft.Boogie.IToken tok, ProofObligationDescription proofObligation) {
-    Range = tok as SourceOrigin ?? (proofObligation as AssertStatementDescription)?.AssertStatement.Origin ?? BoogieGenerator.ToDafnyToken(true, tok);
+    Range = tok as SourceOrigin ?? (proofObligation as AssertStatementDescription)?.AssertStatement.Origin ?? BoogieGenerator.ToDafnyToken(tok);
     ProofObligation = proofObligation;
   }
 }

Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrCall.cs

@@ -225,7 +225,7 @@ void ProcessCallStmt(CallStmt cs, Dictionary<TypeParameter, Type> tySubst, Bpl.E
       directSubstMap.Add(formal, dActual);
       Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(formal.Tok, param, bActual);
       builder.Add(cmd);
-      ins.Add(AdaptBoxing(ToDafnyToken(flags.ReportRanges, param.tok), param, formal.Type.Subst(tySubst), formal.Type));
+      ins.Add(AdaptBoxing(ToDafnyToken(param.tok), param, formal.Type.Subst(tySubst), formal.Type));
     }
 
     // Check that every parameter is available in the state in which the method is invoked; this means checking that it has

Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs

@@ -168,7 +168,7 @@ private bool TrAssertCondition(PredicateStmt stmt,
           if (split.IsChecked) {
             var tok = split.E.tok;
             var desc = new AssertStatementDescription(stmt, errorMessage, successMessage);
-            proofBuilder.Add(AssertAndForget(proofBuilder.Context, ToDafnyToken(flags.ReportRanges, tok), split.E, desc, stmt.Tok,
+            proofBuilder.Add(AssertAndForget(proofBuilder.Context, ToDafnyToken(tok), split.E, desc, stmt.Tok,
               etran.TrAttributes(stmt.Attributes, null))); // attributes go on every split
           }
         }

Source/DafnyDriver/Commands/MeasureComplexityCommand.cs

@@ -112,7 +112,7 @@ public static async Task ReportResourceSummary(
     await output.WriteLineAsync($"The total consumed resources are {totalResources}");
     await output.WriteLineAsync($"The most demanding {worstAmount} verification tasks consumed these resources:");
     foreach (var performer in decreasingWorst) {
-      var location = BoogieGenerator.ToDafnyToken(false, performer.Task.Token).TokenToString(cliCompilation.Options);
+      var location = BoogieGenerator.ToDafnyToken(performer.Task.Token).TokenToString(cliCompilation.Options);
       await output.WriteLineAsync($"{location}: {performer.Result.ResourceCount}");
     }
   }

Source/DafnyDriver/Commands/VerifyCommand.cs

@@ -188,7 +188,7 @@ public static void ReportVerificationDiagnostics(CliCompilation compilation, IOb
       var batchReporter = new BatchErrorReporter(compilation.Options);
       foreach (var completed in result.Results) {
         Compilation.ReportDiagnosticsInResult(compilation.Options, result.CanVerify.FullDafnyName,
-          BoogieGenerator.ToDafnyToken(true, completed.Task.Token),
+          BoogieGenerator.ToDafnyToken(completed.Task.Token),
           (uint)completed.Result.RunTime.TotalSeconds,
           completed.Result, batchReporter);
       }

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs

@@ -293,7 +293,7 @@ string MoreInformation(Boogie.IToken? token, bool hoveringPostcondition) {
           } else {
             token = null;
           }
-          var dafnyToken = BoogieGenerator.ToDafnyToken(true, errorToken);
+          var dafnyToken = BoogieGenerator.ToDafnyToken(errorToken);
 
           // It's not necessary to restate the postcondition itself if the user is already hovering it
           // however, nested postconditions should be displayed

Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs

@@ -46,8 +46,7 @@ public async Task<IReadOnlyList<IVerificationTask>> GetVerificationTasksAsync(Ex
         var boogieProgram = await DafnyMain.LargeStackFactory.StartNew(() => {
           Type.ResetScopes();
           var translatorFlags = new BoogieGenerator.TranslatorFlags(errorReporter.Options) {
-            InsertChecksums = 0 < engine.Options.VerifySnapshots,
-            ReportRanges = program.Options.Get(Snippets.ShowSnippets)
+            InsertChecksums = 0 < engine.Options.VerifySnapshots
           };
           var translator = new BoogieGenerator(errorReporter, resolution.ResolvedProgram.ProofDependencyManager, translatorFlags);
           return translator.DoTranslation(resolution.ResolvedProgram, moduleDefinition);

Source/DafnyLanguageServer/LanguageServer.cs

@@ -49,7 +49,7 @@ related locations
     };
 
     public static void ConfigureDafnyOptionsForServer(DafnyOptions dafnyOptions) {
-      dafnyOptions.Set(Snippets.ShowSnippets, true);
+      dafnyOptions.Set(Snippets.ShowSnippets, false);
     }
 
     public static async Task Start(DafnyOptions dafnyOptions) {

Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs

@@ -380,15 +380,15 @@ previousChild with {
         foreach (var (assertCmd, outcome) in perAssertOutcome) {
           var status = GetNodeStatus(outcome);
           perAssertCounterExample.TryGetValue(assertCmd, out var counterexample);
-          IOrigin? secondaryToken = BoogieGenerator.ToDafnyToken(true, counterexample is ReturnCounterexample returnCounterexample ? returnCounterexample.FailingReturn.tok :
+          IOrigin? secondaryToken = BoogieGenerator.ToDafnyToken(counterexample is ReturnCounterexample returnCounterexample ? returnCounterexample.FailingReturn.tok :
             counterexample is CallCounterexample callCounterexample ? callCounterexample.FailingRequires.tok :
             null);
           if (assertCmd is AssertEnsuresCmd assertEnsuresCmd) {
-            AddChildOutcome(counterexample, assertCmd, BoogieGenerator.ToDafnyToken(true, assertEnsuresCmd.Ensures.tok), status, secondaryToken, " ensures", "_ensures");
+            AddChildOutcome(counterexample, assertCmd, BoogieGenerator.ToDafnyToken(assertEnsuresCmd.Ensures.tok), status, secondaryToken, " ensures", "_ensures");
           } else if (assertCmd is AssertRequiresCmd assertRequiresCmd) {
-            AddChildOutcome(counterexample, assertCmd, BoogieGenerator.ToDafnyToken(true, assertRequiresCmd.Call.tok), status, secondaryToken, assertDisplay: "Call", assertIdentifier: "call");
+            AddChildOutcome(counterexample, assertCmd, BoogieGenerator.ToDafnyToken(assertRequiresCmd.Call.tok), status, secondaryToken, assertDisplay: "Call", assertIdentifier: "call");
           } else {
-            AddChildOutcome(counterexample, assertCmd, BoogieGenerator.ToDafnyToken(true, assertCmd.tok), status, secondaryToken, assertDisplay: "Assertion", assertIdentifier: "assert");
+            AddChildOutcome(counterexample, assertCmd, BoogieGenerator.ToDafnyToken(assertCmd.tok), status, secondaryToken, assertDisplay: "Assertion", assertIdentifier: "assert");
           }
         }
         targetMethodNode.PropagateChildrenErrorsUp();

Source/DafnyLanguageServer/Workspace/Notifications/VerificationDiagnosticsParams.cs

@@ -608,7 +608,7 @@ private AssertionVerificationTree WithImmediatelyRelatedChanges() {
       if (counterExample is ReturnCounterexample returnCounterexample) {
         tok = returnCounterexample.FailingReturn.tok;
         if (tok.filename == assertion.tok.filename) {
-          result.Add(BoogieGenerator.ToDafnyToken(true, returnCounterexample.FailingReturn.tok).StartToken.GetLspRange());
+          result.Add(BoogieGenerator.ToDafnyToken(returnCounterexample.FailingReturn.tok).StartToken.GetLspRange());
         }
       }