Check Reads and Decreases clauses for expressions that could prevent inlining

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));

     }