Simplify error reporting in the trigger generator to get cleaner messages

3 files changed, 8 insertions, 6 deletions

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index 49cd84df..ec2f1777 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -137,9 +137,9 @@ namespace Microsoft.Dafny.Triggers {
     private void CommitOne(QuantifierWithTriggers q, bool addHeader) {

       var errorLevel = ErrorLevel.Info;

       var msg = new StringBuilder();

-      var indent = addHeader ? "   " : " "; //FIXME if multiline messages were properly supported, this indentation wouldn't be needed

+      var indent = addHeader ? "  " : "";

 

-      if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: matchingloop and autotriggers attributes are passed down to Boogie

+      if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: matchingloop, split and autotriggers attributes are passed down to Boogie

         msg.AppendFormat("Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); 

         // FIXME This shouldn't be printed for autoReqs. (see autoReq.dfy)

         // FIXME typeQuantifier?

@@ -156,7 +156,7 @@ namespace Microsoft.Dafny.Triggers {
         AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true);

 

 #if QUANTIFIER_WARNINGS

-        string WARN = (msg.Length > 0 ? indent : "") + (DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) ");

+        string WARN = indent + (DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) ");

         if (!q.CandidateTerms.Any()) {

           errorLevel = ErrorLevel.Warning;

           msg.Append(WARN).AppendLine("No terms found to trigger on.");

@@ -171,7 +171,9 @@ namespace Microsoft.Dafny.Triggers {
       }

       

       if (msg.Length > 0) {

-        reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msg.ToString().TrimEnd("\r\n".ToCharArray()));

+        // Extra indent added to make it easier to distinguish multiline error messages

+        var msgStr = msg.ToString().Replace(Environment.NewLine, Environment.NewLine + " ").TrimEnd("\r\n ".ToCharArray());

+        reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msgStr);

       }

     }

 

diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
index c2e5ef3a..29882da7 100644
--- a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
@@ -1,4 +1,4 @@
-loop-detection-is-not-too-strict.dfy(20,9): Warning:  Selected triggers: {P(x, y)} (loops with {P(x, y + 1)})

+loop-detection-is-not-too-strict.dfy(20,9): Warning: Selected triggers: {P(x, y)} (loops with {P(x, y + 1)})

  (!) Suppressing loops would leave this expression without triggers.

 

 Dafny program verifier finished with 3 verified, 0 errors

diff --git a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
index ef48f568..83648626 100644
--- a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
+++ b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
@@ -1,4 +1,4 @@
-some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning:  Selected triggers: {s[x]} (loops with {s[x + 1]})

+some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning: Selected triggers: {s[x]} (loops with {s[x + 1]})

  (!) Suppressing loops would leave this expression without triggers.

 some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression {x in s ==> s[x + 1] > 0}:

    Selected triggers: {s[x]} (loops with {s[x + 1]})