summaryrefslogtreecommitdiff
path: root/Source/Dafny
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-28 20:39:02 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-28 20:39:02 -0700
commit2db858bf6e72e521b49aa0ae3a993dc943b8c875 (patch)
tree692ebe07028e35e431e8b93ee35266461126d5cd /Source/Dafny
parent3b1c3923a403efbd28b8f5ae6fc4429ccee8c2e8 (diff)
Implement {:nowarn}, clarify some messages, and add a few tests
Diffstat (limited to 'Source/Dafny')
-rw-r--r--Source/Dafny/Triggers/QuantifiersCollection.cs26
-rw-r--r--Source/Dafny/Triggers/TriggerUtils.cs11
2 files changed, 25 insertions, 12 deletions
diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index 50458ab7..f72dab7f 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -117,7 +117,7 @@ namespace Microsoft.Dafny.Triggers {
(candidate, loopingSubterms) => !loopingSubterms.Any(),
(candidate, loopingSubterms) => {
looping.Add(candidate);
- candidate.Annotation = "may loop with " + loopingSubterms.MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", ");
+ candidate.Annotation = "may loop with " + loopingSubterms.MapConcat(t => "\"" + Printer.ExprToString(t.OriginalExpr) + "\"", ", ");
}).ToList();
q.CouldSuppressLoops = safe.Count > 0;
@@ -145,12 +145,14 @@ namespace Microsoft.Dafny.Triggers {
var errorLevel = ErrorLevel.Info;
var msg = new StringBuilder();
var indent = addHeader ? " " : "";
+ bool suppressWarnings = Attributes.Contains(q.quantifier.Attributes, "nowarn");
- if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { // NOTE: matchingloop, split and autotriggers attributes are passed down to Boogie
- msg.AppendFormat("Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine();
+ if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { // NOTE: split and autotriggers attributes are passed down to Boogie
+ var extraMsg = TriggerUtils.WantsAutoTriggers(q.quantifier) ? "" : " Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.";
+ msg.AppendFormat("Not generating triggers for \"{0}\".{1}", Printer.ExprToString(q.quantifier.Term), extraMsg).AppendLine();
} else {
if (addHeader) {
- msg.AppendFormat("For expression {{{0}}}:", Printer.ExprToString(q.quantifier.Term)).AppendLine();
+ msg.AppendFormat("For expression \"{0}\":", Printer.ExprToString(q.quantifier.Term)).AppendLine();
}
foreach (var candidate in q.Candidates) {
@@ -161,20 +163,26 @@ namespace Microsoft.Dafny.Triggers {
AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true);
#if QUANTIFIER_WARNINGS
- string WARN = indent + (DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) ");
+ var WARN_TAG = DafnyOptions.O.UnicodeOutput ? "⚠ " : "/!\\ ";
+ var WARN_TAG_OVERRIDE = suppressWarnings ? "(Suppressed warning) " : WARN_TAG;
+ var WARN_LEVEL = suppressWarnings ? ErrorLevel.Info : ErrorLevel.Warning;
+ var WARN = indent + WARN_TAG_OVERRIDE;
if (!q.CandidateTerms.Any()) {
- errorLevel = ErrorLevel.Warning;
+ errorLevel = WARN_LEVEL;
msg.Append(WARN).AppendLine("No terms found to trigger on.");
} else if (!q.Candidates.Any()) {
- errorLevel = ErrorLevel.Warning;
+ errorLevel = WARN_LEVEL;
msg.Append(WARN).AppendLine("No trigger covering all quantified variables found.");
} else if (!q.CouldSuppressLoops && !q.AllowsLoops) {
- errorLevel = ErrorLevel.Warning;
+ errorLevel = WARN_LEVEL;
msg.Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers.");
+ } else if (suppressWarnings) {
+ errorLevel = ErrorLevel.Warning;
+ msg.Append(indent).Append(WARN_TAG).AppendLine("There is no warning here to suppress.");
}
#endif
}
-
+
if (msg.Length > 0) {
var msgStr = msg.ToString().TrimEnd("\r\n ".ToCharArray());
reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msgStr);
diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
index efa1f167..c16a3e44 100644
--- a/Source/Dafny/Triggers/TriggerUtils.cs
+++ b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -183,14 +183,19 @@ namespace Microsoft.Dafny.Triggers {
internal static bool AllowsMatchingLoops(QuantifierExpr quantifier) {
Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier
+ // This is different from nowarn: it won't remove loops at all, even if another trigger is available.
return Attributes.Contains(quantifier.Attributes, "matchingloop");
}
- internal static bool NeedsAutoTriggers(QuantifierExpr quantifier) {
+ internal static bool WantsAutoTriggers(QuantifierExpr quantifier) {
Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier
bool wantsAutoTriggers = true;
- return !Attributes.Contains(quantifier.Attributes, "trigger") &&
- (!Attributes.ContainsBool(quantifier.Attributes, "autotriggers", ref wantsAutoTriggers) || wantsAutoTriggers);
+ return !Attributes.ContainsBool(quantifier.Attributes, "autotriggers", ref wantsAutoTriggers) || wantsAutoTriggers;
+ }
+
+ internal static bool NeedsAutoTriggers(QuantifierExpr quantifier) {
+ Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier
+ return !Attributes.Contains(quantifier.Attributes, "trigger") && WantsAutoTriggers(quantifier);
}
internal static BinaryExpr.ResolvedOpcode RemoveNotInBinaryExprIn(BinaryExpr.ResolvedOpcode opcode) {