diff options
author | 2011-05-26 23:40:33 -0700 | |
---|---|---|
committer | 2011-05-26 23:40:33 -0700 | |
commit | c6d9da6f688c18844c7f6a471030cce513e848b0 (patch) | |
tree | 60c06c7fabf5e9fef54cb4889d896454f535b5af /Source/Dafny/DafnyAst.cs | |
parent | cb83cf98d04830e986a101246b3a0a7180a06d36 (diff) |
Dafny:
* fixed ghost/non-ghost story for breaks and returns
* changed compilation/translation to always use goto's to implement Dafny's breaks
* introduced "break break" statements
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 49 |
1 files changed, 31 insertions, 18 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 8d1143af..bb5f4f67 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1141,6 +1141,8 @@ namespace Microsoft.Dafny { public abstract class Statement {
public readonly IToken Tok;
+ public LabelNode Labels; // mutable during resolution
+
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Tok != null);
@@ -1153,7 +1155,25 @@ namespace Microsoft.Dafny { }
}
- public abstract class PredicateStmt : Statement {
+ public class LabelNode
+ {
+ public readonly IToken Tok;
+ public readonly string Label;
+ public readonly int UniqueId;
+ public readonly LabelNode Next;
+ static int nodes = 0;
+
+ public LabelNode(IToken tok, string label, LabelNode next) {
+ Contract.Requires(tok != null);
+ Tok = tok;
+ Label = label;
+ Next = next;
+ UniqueId = nodes++;
+ }
+ }
+
+ public abstract class PredicateStmt : Statement
+ {
[Peer]
public readonly Expression Expr;
[ContractInvariantMethod]
@@ -1255,31 +1275,25 @@ namespace Microsoft.Dafny { }
}
- public class LabelStmt : Statement {
- public readonly string Label;
+ public class BreakStmt : Statement {
+ public readonly string TargetLabel;
+ public readonly int BreakCount;
+ public Statement TargetStmt; // filled in during resolution
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(Label != null);
+ Contract.Invariant(TargetLabel == null || 1 <= BreakCount);
}
- public LabelStmt(IToken/*!*/ tok, string/*!*/ label)
+ public BreakStmt(IToken tok, string targetLabel)
: base(tok) {
Contract.Requires(tok != null);
- Contract.Requires(label != null);
- this.Label = label;
-
+ this.TargetLabel = targetLabel;
}
- }
-
- public class BreakStmt : Statement {
- public readonly string TargetLabel;
- public Statement TargetStmt; // filled in during resolution
-
- public BreakStmt(IToken tok, string targetLabel)
+ public BreakStmt(IToken tok, int breakCount)
: base(tok) {
Contract.Requires(tok != null);
- this.TargetLabel = targetLabel;
-
+ Contract.Requires(1 <= breakCount);
+ this.BreakCount = breakCount;
}
}
@@ -1287,7 +1301,6 @@ namespace Microsoft.Dafny { public ReturnStmt(IToken tok)
: base(tok) {
Contract.Requires(tok != null);
-
}
}
|