diff options
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]})
|