diff options
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 6 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 2 |
2 files changed, 8 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));
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 55dd637c..50324002 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -13126,6 +13126,8 @@ namespace Microsoft.Dafny { visitor.Visit(f.Body);
foreach (var expr in f.Ens) { visitor.Visit(expr); }
foreach (var expr in f.Req) { visitor.Visit(expr); }
+ foreach (var expr in f.Reads) { visitor.Visit(expr); }
+ foreach (var expr in f.Decreases.Expressions) { visitor.Visit(expr); }
return f.Formals.Zip(fexp.Args).All(formal_concrete => CanSafelySubstitute(visitor.TriggerVariables, formal_concrete.Item1, formal_concrete.Item2));
}
|