summaryrefslogtreecommitdiff
path: root/Source/Dafny
diff options
context:
space:
mode:
authorGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-09-10 18:37:47 -0700
committerGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-09-10 18:37:47 -0700
commitfc76541682ec019b8a2dc08ca9972ff517db9b74 (patch)
tree5c1031bdadd59e5c6a05b960cb2dabbb2070a56e /Source/Dafny
parentbef7f2ff0dbe833b157970efa16b12086776ef70 (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)
Diffstat (limited to 'Source/Dafny')
-rw-r--r--Source/Dafny/Compiler.cs2
-rw-r--r--Source/Dafny/RefinementTransformer.cs15
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;