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/Translator.cs | |
parent | 045ee27da6435a6262edbada4f7911b2f3ff45b8 (diff) |
Check Reads and Decreases clauses for expressions that could prevent inlining
Diffstat (limited to 'Source/Dafny/Translator.cs')
-rw-r--r-- | Source/Dafny/Translator.cs | 2 |
1 files changed, 2 insertions, 0 deletions
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));
}
|