diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-10 18:37:47 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-10 18:37:47 -0700 |
| commit | fc76541682ec019b8a2dc08ca9972ff517db9b74 (patch) | |
| tree | 5c1031bdadd59e5c6a05b960cb2dabbb2070a56e | |
| parent | bef7f2ff0dbe833b157970efa16b12086776ef70 (diff) | |
Dafny: did a little to extend the support of labeled statements in refinements (things like multiple labels are still not thought through very well)
| -rw-r--r-- | Source/Dafny/Compiler.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 15 |
2 files changed, 13 insertions, 4 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 8715c047..a138f4d9 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -637,7 +637,7 @@ namespace Microsoft.Dafny { if (m.IsTailRecursive) {
Indent(indent); wr.WriteLine("TAIL_CALL_START: ;");
if (!m.IsStatic) {
- Indent(indent); wr.WriteLine("var _this = this;");
+ Indent(indent + IndentAmount); wr.WriteLine("var _this = this;");
}
}
Contract.Assert(enclosingMethod == null);
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 60aa1bfd..31ecfc9c 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -785,8 +785,6 @@ namespace Microsoft.Dafny *
* Note, LoopSpec must contain only invariant declarations (as the parser ensures for the first three cases).
* Note, there is an implicit "...;" at the end of every block in a skeleton.
- *
- * TODO: should also handle labels and some form of new "replace" statement
*/
if (cur is SkeletonStatement) {
var S = ((SkeletonStatement)cur).S;
@@ -1071,10 +1069,21 @@ namespace Microsoft.Dafny }
bool PotentialMatch(Statement nxt, Statement other) {
+ Contract.Requires(nxt != null);
Contract.Requires(!(nxt is SkeletonStatement) || ((SkeletonStatement)nxt).S != null); // nxt is not "...;"
Contract.Requires(other != null);
- if (nxt is SkeletonStatement) {
+ if (nxt.Labels != null) {
+ for (var olbl = other.Labels; olbl != null; olbl = olbl.Next) {
+ var odata = olbl.Data;
+ for (var l = nxt.Labels; l != null; l = l.Next) {
+ if (odata.Name == l.Data.Name) {
+ return true;
+ }
+ }
+ }
+ return false; // labels of 'nxt' don't match any label of 'other'
+ } else if (nxt is SkeletonStatement) {
var S = ((SkeletonStatement)nxt).S;
if (S is AssertStmt) {
return other is PredicateStmt;
|