diff options
author | leino <unknown> | 2015-11-28 22:22:52 -0800 |
---|---|---|
committer | leino <unknown> | 2015-11-28 22:22:52 -0800 |
commit | 8131e68401d9f97d1216be32f3d0e23db83da744 (patch) | |
tree | e81ce9c5d05683a219712456852d64e7af767e62 /Source | |
parent | 33ae6b4bf0dc3f2c80abbd3c26356f16ded3aaee (diff) |
Made an adjustment in the printing of resolved forall expressions (previous code introduced
with bug fix 103 and tripped over with the /rprint and /autoTriggers:1 flags used in the new
dafny4/UnionFind.dfy test).
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Dafny/Printer.cs | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 0a25b941..6010e2f0 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -846,10 +846,7 @@ namespace Microsoft.Dafny { if (attributes == null && s.ForallExpressions != null) {
foreach (Expression expr in s.ForallExpressions) {
ForallExpr e = (ForallExpr)expr;
- while (e != null && attributes == null) {
- attributes = e.Attributes;
- e = (ForallExpr)e.SplitQuantifierExpression;
- }
+ attributes = GetSomeAttributes(e);
if (attributes != null) { break; }
}
} @@ -1010,6 +1007,20 @@ namespace Microsoft.Dafny { } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement } + }
+
+ private static Attributes GetSomeAttributes(Expression expr) {
+ if (expr is ForallExpr) {
+ var e = (ForallExpr)expr;
+ if (e.Attributes != null) {
+ return e.Attributes;
+ }
+ return GetSomeAttributes(e.SplitQuantifierExpression);
+ } else if (expr is BinaryExpr) {
+ var e = (BinaryExpr)expr;
+ return GetSomeAttributes(e.E0) ?? GetSomeAttributes(e.E1);
+ }
+ return null;
} private void PrintModifyStmt(int indent, ModifyStmt s, bool omitFrame) { |