Don't say "error is impossible" anymore (dafny-lang#4292)

This was a confusing message and it's possible to do better.

This addresses dafny-lang#3954, but I don't think it entirely resolves it. To do
that, I think it'd be best to extend ProofObligationDescription to
include related locations, which will require Boogie changes.

This change helps the situation in the meantime, however.

By submitting this pull request, I confirm that my contribution is made
under the terms of the MIT license.

Source/DafnyCore/Verifier/ProofObligationDescription.cs

@@ -1107,17 +1107,15 @@ public AssignmentShrinks(string fieldName) {
   }
 }
 
-public class BoilerplateTriple : ProofObligationDescriptionWithNoExpr {
-  public override string SuccessDescription =>
-    $"error is impossible: {msg}";
-
-  public override string FailureDescription => msg;
-
+public class BoilerplateTriple : ProofObligationDescriptionCustomMessages {
   public override string ShortDescription => "boilerplate triple";
 
-  private readonly string msg;
+  public override string DefaultSuccessDescription { get; }
+  public override string DefaultFailureDescription { get; }
 
-  public BoilerplateTriple(string msg) {
-    this.msg = msg;
+  public BoilerplateTriple(string errorMessage, string successMessage, string comment)
+    : base(errorMessage, successMessage) {
+    this.DefaultSuccessDescription = comment;
+    this.DefaultFailureDescription = comment;
   }
 }

Source/DafnyCore/Verifier/Translator.TrStatement.cs

@@ -1444,7 +1444,7 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr,
             invariants.Add(TrAssumeCmd(s.Tok, tri.Expr));
           } else {
             Contract.Assert(tri.ErrorMessage != null);  // follows from BoilerplateTriple invariant
-            invariants.Add(Assert(s.Tok, tri.Expr, new PODesc.BoilerplateTriple(tri.ErrorMessage)));
+            invariants.Add(Assert(s.Tok, tri.Expr, new PODesc.BoilerplateTriple(tri.ErrorMessage, tri.SuccessMessage, tri.Comment)));
           }
         }
         // add a free invariant which says that the heap hasn't changed outside of the modifies clause.

Test/logger/TripleDescription.dfy

@@ -0,0 +1,13 @@
+// RUN: %exits-with 4 %baredafny verify --show-snippets:false --log-format:text "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK: Outcome: Invalid
+// CHECK: TripleDescription.dfy(.*,.*): this postcondition holds
+method BadAbs(x: int) returns (r: int)
+  ensures r > 0
+{
+    if(x < 0) {
+        return -x;
+    } else {
+        return x;
+    }
+}