Adapted to the new ProofObligationDescription

dafny-lang · Apr 15, 2022 · 1979d03 · 1979d03
1 parent e7537ad
commit 1979d03
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 11 deletions.
diff --git a/Source/Dafny/Verifier/ProofObligationDescription.cs b/Source/Dafny/Verifier/ProofObligationDescription.cs
@@ -244,14 +244,17 @@ customErrMsg is null
       : $"error is impossible: {customErrMsg}";
 
   public override string FailureDescription =>
-    customErrMsg ?? "function precondition might not hold";
+    (customErrMsg ?? "function precondition might not hold") + (optionalHint ?? "");
 
   public override string ShortDescription => "precondition";
 
   private readonly string customErrMsg;
 
-  public PreconditionSatisfied([CanBeNull] string customErrMsg) {
+  private readonly string optionalHint;
+
+  public PreconditionSatisfied([CanBeNull] string customErrMsg, [CanBeNull] string optionalHint = null) {
     this.customErrMsg = customErrMsg;
+    this.optionalHint = optionalHint;
   }
 }
 

diff --git a/Source/Dafny/Verifier/Translator.cs b/Source/Dafny/Verifier/Translator.cs
@@ -5763,6 +5763,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu
             Expression precond = Substitute(p.E, e.Receiver, substMap, e.GetTypeArgumentSubstitutions());
             bool splitHappened;  // we don't actually care
             string errorMessage = CustomErrorMessage(p.Attributes);
+            string optionalHint = null;
             foreach (var ss in TrSplitExpr(precond, etran, true, out splitHappened)) {
               if (ss.IsChecked) {
                 var tok = new NestedToken(GetToken(expr), ss.E.tok);
@@ -5772,20 +5773,19 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu
                           subExpression is IdentifierExpr v &&
                           v.Var.CompileName == entry.Key
                         )) {
-                      errorMessage = $"possible violation of function precondition." +
-                                     $" Careful: variable {entry.Value.DisplayName} has type {entry.Value.CompilableType}" +
+                      optionalHint = $". Careful: variable {entry.Value.DisplayName} has type {entry.Value.CompilableType}" +
                                      $" and not {entry.Value.OriginalType} because the range is compiled" +
                                      $" and {entry.Value.OriginalType} cannot be tested at run-time";
                       break;
                     }
                   }
                 }
-                var desc = new PODesc.PreconditionSatisfied(errorMessage);
+                var desc = new PODesc.PreconditionSatisfied(errorMessage, optionalHint);
                 if (options.AssertKv != null) {
                   // use the given assert attribute only
-                  builder.Add(Assert(tok, ss.E, new PODesc.PreconditionSatisfied(errorMessage), options.AssertKv));
+                  builder.Add(Assert(tok, ss.E, desc, options.AssertKv));
                 } else {
-                  builder.Add(AssertNS(tok, ss.E, new PODesc.PreconditionSatisfied(errorMessage)));
+                  builder.Add(AssertNS(tok, ss.E, desc));
                 }
               }
             }

diff --git a/Test/git-issues/git-issue-1604g.dfy.expect b/Test/git-issues/git-issue-1604g.dfy.expect
@@ -1,18 +1,18 @@
 git-issue-1604g.dfy(38,8): Error: Could not prove that the range constrains the bound variable 'f' to be of type SpecialFruit, and since SpecialFruit is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Fruit.
 git-issue-1604g.dfy(16,31): [Related location] SpecialFruit is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')
-git-issue-1604g.dfy(38,40): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time
+git-issue-1604g.dfy(38,40): Error: function precondition might not hold. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time
 git-issue-1604g.dfy(19,11): Related location
 git-issue-1604g.dfy(13,2): Related location
 git-issue-1604g.dfy(8,25): Related location
-git-issue-1604g.dfy(38,40): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time
+git-issue-1604g.dfy(38,40): Error: function precondition might not hold. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time
 git-issue-1604g.dfy(19,11): Related location
 git-issue-1604g.dfy(13,2): Related location
 git-issue-1604g.dfy(9,19): Related location
-git-issue-1604g.dfy(42,30): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time
+git-issue-1604g.dfy(42,30): Error: function precondition might not hold. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time
 git-issue-1604g.dfy(19,11): Related location
 git-issue-1604g.dfy(13,2): Related location
 git-issue-1604g.dfy(8,25): Related location
-git-issue-1604g.dfy(42,30): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time
+git-issue-1604g.dfy(42,30): Error: function precondition might not hold. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time
 git-issue-1604g.dfy(19,11): Related location
 git-issue-1604g.dfy(13,2): Related location
 git-issue-1604g.dfy(9,19): Related location