1 files changed, 92 insertions, 0 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 1c43a530..223e0b28 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1665,6 +1665,13 @@ namespace Microsoft.Dafny {
     public virtual IEnumerable<Statement> SubStatements {
       get { yield break; }
     }
+
+    /// <summary>
+    /// Returns the non-null expressions of this statement proper (that is, do not include the expressions of substatements).
+    /// </summary>
+    public virtual IEnumerable<Expression> SubExpressions {
+      get { yield break; }
+    }
   }
 
   public class LList<T>
@@ -1729,6 +1736,11 @@ namespace Microsoft.Dafny {
       Contract.Requires(expr != null);
       this.Expr = expr;
     }
+    public override IEnumerable<Expression> SubExpressions {
+      get {
+        yield return Expr;
+      }
+    }
   }
 
   public class AssertStmt : PredicateStmt {
@@ -1761,6 +1773,15 @@ namespace Microsoft.Dafny {
 
       Args = args;
     }
+    public override IEnumerable<Expression> SubExpressions {
+      get {
+        foreach (var arg in Args) {
+          if (arg.E != null) {
+            yield return arg.E;
+          }
+        }
+      }
+    }
   }
 
   public class BreakStmt : Statement {
@@ -1795,6 +1816,15 @@ namespace Microsoft.Dafny {
       this.rhss = rhss;
       hiddenUpdate = null;
     }
+    public override IEnumerable<Expression> SubExpressions {
+      get {
+        foreach (var rhs in rhss) {
+          foreach (var ee in rhs.SubExpressions) {
+            yield return ee;
+          }
+        }
+      }
+    }
   }
 
   public abstract class AssignmentRhs {
@@ -2103,6 +2133,15 @@ namespace Microsoft.Dafny {
       }
     }
 
+    public override IEnumerable<Expression> SubExpressions {
+      get {
+        yield return Lhs;
+        foreach (var ee in Rhs.SubExpressions) {
+          yield return ee;
+        }
+      }
+    }
+
     /// <summary>
     /// This method assumes "lhs" has been successfully resolved.
     /// </summary>
@@ -2221,6 +2260,18 @@ namespace Microsoft.Dafny {
       this.MethodName = methodName;
       this.Args = args;
     }
+
+    public override IEnumerable<Expression> SubExpressions {
+      get {
+        foreach (var ee in Lhs) {
+          yield return ee;
+        }
+        yield return Receiver;
+        foreach (var ee in Args) {
+          yield return ee;
+        }
+      }
+    }
   }
 
   public class BlockStmt : Statement {
@@ -2263,6 +2314,13 @@ namespace Microsoft.Dafny {
         }
       }
     }
+    public override IEnumerable<Expression> SubExpressions {
+      get {
+        if (Guard != null) {
+          yield return Guard;
+        }
+      }
+    }
   }
 
   public class GuardedAlternative
@@ -2309,6 +2367,13 @@ namespace Microsoft.Dafny {
         }
       }
     }
+    public override IEnumerable<Expression> SubExpressions {
+      get {
+        foreach (var alt in Alternatives) {
+          yield return alt.Guard;
+        }
+      }
+    }
   }
 
   public abstract class LoopStmt : Statement
@@ -2360,6 +2425,13 @@ namespace Microsoft.Dafny {
         yield return Body;
       }
     }
+    public override IEnumerable<Expression> SubExpressions {
+      get {
+        if (Guard != null) {
+          yield return Guard;
+        }
+      }
+    }
   }
 
   /// <summary>
@@ -2401,6 +2473,13 @@ namespace Microsoft.Dafny {
         }
       }
     }
+    public override IEnumerable<Expression> SubExpressions {
+      get {
+        foreach (var alt in Alternatives) {
+          yield return alt.Guard;
+        }
+      }
+    }
   }
 
   public class ParallelStmt : Statement
@@ -2482,6 +2561,14 @@ namespace Microsoft.Dafny {
         yield return Body;
       }
     }
+    public override IEnumerable<Expression> SubExpressions {
+      get {
+        yield return Range;
+        foreach (var ee in Ens) {
+          yield return ee.E;
+        }
+      }
+    }
   }
 
   public class MatchStmt : Statement
@@ -2515,6 +2602,11 @@ namespace Microsoft.Dafny {
         }
       }
     }
+    public override IEnumerable<Expression> SubExpressions {
+      get {
+        yield return Source;
+      }
+    }
   }
 
   public class MatchCaseStmt : MatchCase