diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-18 09:35:23 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-18 09:35:23 -0700 |
| commit | 8a1ae35f1f4282573fa8b67e1151b0cbbabeb136 (patch) | |
| tree | d4ffde34cc738f1e9f1e4e40ddd04c2f4a6f0dd4 /Source/Dafny/DafnyAst.cs | |
| parent | 045ee27da6435a6262edbada4f7911b2f3ff45b8 (diff) | |
Check Reads and Decreases clauses for expressions that could prevent inlining
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index a902a18c..e5d8250b 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -7674,6 +7674,9 @@ namespace Microsoft.Dafny { public void Visit(MaybeFreeExpression expr) {
Visit(expr.E);
}
+ public void Visit(FrameExpression expr) {
+ Visit(expr.E);
+ }
public void Visit(IEnumerable<MaybeFreeExpression> exprs) {
exprs.Iter(Visit);
}
@@ -7717,6 +7720,9 @@ namespace Microsoft.Dafny { public void Visit(MaybeFreeExpression expr, State st) {
Visit(expr.E, st);
}
+ public void Visit(FrameExpression expr, State st) {
+ Visit(expr.E, st);
+ }
public void Visit(IEnumerable<MaybeFreeExpression> exprs, State st) {
exprs.Iter(e => Visit(e, st));
}
|