From fde628b5153b86f187f353c6f79113932c309abe Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 17 Jul 2015 14:08:12 -0700 Subject: Add /autoTriggers to TriggerInPredicate's RUN specification --- Test/dafny0/TriggerInPredicate.dfy | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 Test/dafny0/TriggerInPredicate.dfy (limited to 'Test/dafny0/TriggerInPredicate.dfy') diff --git a/Test/dafny0/TriggerInPredicate.dfy b/Test/dafny0/TriggerInPredicate.dfy new file mode 100644 index 00000000..3f2eac2c --- /dev/null +++ b/Test/dafny0/TriggerInPredicate.dfy @@ -0,0 +1,19 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +predicate A(x: bool, y: bool) { x } + +predicate B(x: bool, z: bool) { forall y {:trigger A(x, y) } :: A(x, y) && z } + +// Inlining is disabled here to prevent pollution of the trigger in B +method C() requires B(true || false, true) {} + +// Inlining should work fine here +method C'() requires B(true, true) {} + +// Inlining should work fine here +method C''() requires B(true, true && false) {} + +// Local Variables: +// dafny-prover-local-args: ("/autoTriggers:1") +// End: -- cgit v1.2.3 From b4f926f38536d30b7d12c35cbf8f45fa7ef71c27 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 19 Aug 2015 10:37:49 -0700 Subject: Cleanup indentation of trigger warnings --- Source/Dafny/Triggers/QuantifiersCollection.cs | 12 ++++++------ Test/dafny0/TriggerInPredicate.dfy | 2 +- Test/dafny0/TriggerInPredicate.dfy.expect | 2 ++ 3 files changed, 9 insertions(+), 7 deletions(-) (limited to 'Test/dafny0/TriggerInPredicate.dfy') diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index 01bceeb7..aa008e36 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -138,12 +138,12 @@ namespace Microsoft.Dafny.Triggers { var indent = addHeader ? " " : " "; //FIXME if multiline messages were properly supported, this indentation wouldn't be needed if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: matchingloop and autotriggers attributes are passed down to Boogie - msg.AppendFormat(" Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); + 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? } 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) { //FIXME make this _trigger instead of trigger @@ -154,16 +154,16 @@ namespace Microsoft.Dafny.Triggers { AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true); #if QUANTIFIER_WARNINGS - string WARN = DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) "; //FIXME set unicodeoutput in extension + string WARN = (msg.Length > 0 ? indent : "") + (DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) "); //FIXME set unicodeoutput in extension if (!q.CandidateTerms.Any()) { errorLevel = ErrorLevel.Warning; - msg.Append(indent).Append(WARN).AppendLine("No terms found to trigger on."); + msg.Append(WARN).AppendLine("No terms found to trigger on."); } else if (!q.Candidates.Any()) { errorLevel = ErrorLevel.Warning; - msg.Append(indent).Append(WARN).AppendLine("No trigger covering all quantified variables found."); + msg.Append(WARN).AppendLine("No trigger covering all quantified variables found."); } else if (!q.CouldSuppressLoops && !q.AllowsLoops) { errorLevel = ErrorLevel.Warning; - msg.Append(indent).Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers."); + msg.Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers."); } #endif } diff --git a/Test/dafny0/TriggerInPredicate.dfy b/Test/dafny0/TriggerInPredicate.dfy index 3f2eac2c..b9c372dc 100644 --- a/Test/dafny0/TriggerInPredicate.dfy +++ b/Test/dafny0/TriggerInPredicate.dfy @@ -3,7 +3,7 @@ predicate A(x: bool, y: bool) { x } -predicate B(x: bool, z: bool) { forall y {:trigger A(x, y) } :: A(x, y) && z } +predicate B(x: bool, z: bool) { forall y {:trigger A(x, y)} :: A(x, y) && z } // Inlining is disabled here to prevent pollution of the trigger in B method C() requires B(true || false, true) {} diff --git a/Test/dafny0/TriggerInPredicate.dfy.expect b/Test/dafny0/TriggerInPredicate.dfy.expect index 7f6e0268..1cbd4034 100644 --- a/Test/dafny0/TriggerInPredicate.dfy.expect +++ b/Test/dafny0/TriggerInPredicate.dfy.expect @@ -1,3 +1,5 @@ +TriggerInPredicate.dfy(6,32): Info: Not generating triggers for {A(x, y)}. +TriggerInPredicate.dfy(6,32): Info: Not generating triggers for {z}. TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined. TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined. -- cgit v1.2.3