diff options
| author |  Rustan Leino <unknown> | 2015-08-20 18:15:24 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-08-20 18:15:24 -0700 |
| commit | c90ce03a868baeb34de89a4fb73c5001dc737bec (patch) | |
| tree | b7e947a8c6d40bce0fce34521cfc1804e6c59fdc /Source/Dafny/DafnyAst.cs | |
| parent | efcd1e908cb7ea05e78faffd206fa5ce1e966b74 (diff) | |
| parent | 24812516d64ed809d7446680a79eac492ea6a201 (diff) | |
Merge
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index d78ae170..5943e8e4 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -7764,6 +7764,33 @@ namespace Microsoft.Dafny { public void Visit(IEnumerable<MaybeFreeExpression> exprs) {
exprs.Iter(Visit);
}
+ public void Visit(IEnumerable<FrameExpression> exprs) {
+ exprs.Iter(Visit);
+ }
+ public void Visit(ICallable decl) {
+ if (decl is Function) {
+ Visit((Function)decl);
+ } else if (decl is Method) {
+ Visit((Method)decl);
+ }
+ //FIXME More?
+ }
+ public void Visit(Method method) {
+ Visit(method.Ens);
+ Visit(method.Req);
+ Visit(method.Mod.Expressions);
+ Visit(method.Decreases.Expressions);
+ if (method.Body != null) { Visit(method.Body); }
+ //FIXME More?
+ }
+ public void Visit(Function function) {
+ Visit(function.Ens);
+ Visit(function.Req);
+ Visit(function.Reads);
+ Visit(function.Decreases.Expressions);
+ if (function.Body != null) { Visit(function.Body); }
+ //FIXME More?
+ }
protected virtual void VisitOneExpr(Expression expr) {
Contract.Requires(expr != null);
// by default, do nothing
@@ -7810,6 +7837,33 @@ namespace Microsoft.Dafny { public void Visit(IEnumerable<MaybeFreeExpression> exprs, State st) {
exprs.Iter(e => Visit(e, st));
}
+ public void Visit(IEnumerable<FrameExpression> exprs, State st) {
+ exprs.Iter(e => Visit(e, st));
+ }
+ public void Visit(ICallable decl, State st) {
+ if (decl is Function) {
+ Visit((Function)decl, st);
+ } else if (decl is Method) {
+ Visit((Method)decl, st);
+ }
+ //FIXME More?
+ }
+ public void Visit(Method method, State st) {
+ Visit(method.Ens, st);
+ Visit(method.Req, st);
+ Visit(method.Mod.Expressions, st);
+ Visit(method.Decreases.Expressions, st);
+ if (method.Body != null) { Visit(method.Body, st); }
+ //FIXME More?
+ }
+ public void Visit(Function function, State st) {
+ Visit(function.Ens, st);
+ Visit(function.Req, st);
+ Visit(function.Reads, st);
+ Visit(function.Decreases.Expressions, st);
+ if (function.Body != null) { Visit(function.Body, st); }
+ //FIXME More?
+ }
/// <summary>
/// Visit one expression proper. This method is invoked before it is invoked on the
/// sub-parts (sub-expressions and sub-statements). A return value of "true" says to
|