diff options
| author |  Rustan Leino <unknown> | 2014-04-04 07:01:32 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-04-04 07:01:32 -0700 |
| commit | 390da153fcba46e4cd511adda888a3920af56862 (patch) | |
| tree | 8c5db48aaed9624a09cab1017c896ae79738fd10 /Source/Dafny/DafnyAst.cs | |
| parent | cd206ac033a1e369277f824dd3a13eca32f0396c (diff) | |
Added "modify Frame { Body }" statement.
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index c3ff26db..51449440 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -3510,16 +3510,25 @@ namespace Microsoft.Dafny { public class ModifyStmt : Statement
{
public readonly Specification<FrameExpression> Mod;
+ public readonly BlockStmt Body;
- public ModifyStmt(IToken tok, IToken endTok, List<FrameExpression> mod, Attributes attrs)
+ public ModifyStmt(IToken tok, IToken endTok, List<FrameExpression> mod, Attributes attrs, BlockStmt body)
: base(tok, endTok)
{
Contract.Requires(tok != null);
Contract.Requires(endTok != null);
Contract.Requires(mod != null);
- Mod = new Specification<FrameExpression>(mod, attrs);
+ Mod = new Specification<FrameExpression>(mod, attrs);
+ Body = body;
}
+ public override IEnumerable<Statement> SubStatements {
+ get {
+ if (Body != null) {
+ yield return Body;
+ }
+ }
+ }
public override IEnumerable<Expression> SubExpressions {
get {
foreach (var fe in Mod.Expressions) {
|