Implement {:nowarn}, clarify some messages, and add a few tests

1 files changed, 8 insertions, 3 deletions

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) {