diff options
| -rw-r--r-- | Dafny/Resolver.ssc | 42 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 17 | ||||
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 2 | ||||
| -rw-r--r-- | Util/latex/dafny.sty | 4 | ||||
| -rw-r--r-- | Util/vim/syntax/dafny.vim | 6 |
6 files changed, 53 insertions, 24 deletions
diff --git a/Dafny/Resolver.ssc b/Dafny/Resolver.ssc index 96ae33c6..58992dea 100644 --- a/Dafny/Resolver.ssc +++ b/Dafny/Resolver.ssc @@ -624,7 +624,9 @@ namespace Microsoft.Dafny { // any type is fine
}
- // Add out-parameters to the scope, but don't care about any duplication errors, since they have already been reported
+ // Add out-parameters to a new scope that will also include the outermost-level locals of the body
+ // Don't care about any duplication errors among the out-parameters, since they have already been reported
+ scope.PushMarker();
foreach (Formal p in m.Outs) {
scope.Push(p.Name, p);
}
@@ -640,10 +642,11 @@ namespace Microsoft.Dafny { // Resolve body
if (m.Body != null) {
- ResolveStatement(m.Body, m.IsGhost, m);
+ ResolveBlockStatement(m.Body, m.IsGhost, m);
}
- scope.PopMarker();
+ scope.PopMarker(); // for the out-parameters and outermost-level locals
+ scope.PopMarker(); // for the in-parameters
}
/// <summary>
@@ -1254,20 +1257,7 @@ namespace Microsoft.Dafny { } else if (stmt is BlockStmt) {
scope.PushMarker();
- int labelsToPop = 0;
- foreach (Statement ss in ((BlockStmt)stmt).Body) {
- if (ss is LabelStmt) {
- LabelStmt ls = (LabelStmt)ss;
- labeledStatements.PushMarker();
- bool b = labeledStatements.Push(ls.Label, ls);
- assert b; // since we just pushed a marker, we expect the Push to succeed
- labelsToPop++;
- } else {
- ResolveStatement(ss, specContextOnly, method);
- for (; 0 < labelsToPop; labelsToPop--) { labeledStatements.PopMarker(); }
- }
- }
- for (; 0 < labelsToPop; labelsToPop--) { labeledStatements.PopMarker(); }
+ ResolveBlockStatement((BlockStmt)stmt, specContextOnly, method);
scope.PopMarker();
} else if (stmt is IfStmt) {
@@ -1452,6 +1442,24 @@ namespace Microsoft.Dafny { }
}
+ void ResolveBlockStatement(BlockStmt! blockStmt, bool specContextOnly, Method! method)
+ {
+ int labelsToPop = 0;
+ foreach (Statement ss in blockStmt.Body) {
+ if (ss is LabelStmt) {
+ LabelStmt ls = (LabelStmt)ss;
+ labeledStatements.PushMarker();
+ bool b = labeledStatements.Push(ls.Label, ls);
+ assert b; // since we just pushed a marker, we expect the Push to succeed
+ labelsToPop++;
+ } else {
+ ResolveStatement(ss, specContextOnly, method);
+ for (; 0 < labelsToPop; labelsToPop--) { labeledStatements.PopMarker(); }
+ }
+ }
+ for (; 0 < labelsToPop; labelsToPop--) { labeledStatements.PopMarker(); }
+ }
+
Type! ResolveTypeRhs(TypeRhs! rr, Statement! stmt, bool specContext) {
ResolveType(rr.EType);
if (rr.ArraySize == null) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 0f980af2..82f1da59 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -75,7 +75,11 @@ TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C TypeTests.dfy(20,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nothing' can be constructed
TypeTests.dfy(23,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
TypeTests.dfy(55,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-10 resolution/type errors detected in TypeTests.dfy
+TypeTests.dfy(64,6): Error: Duplicate local-variable name: z
+TypeTests.dfy(66,6): Error: Duplicate local-variable name: x
+TypeTests.dfy(69,8): Error: Duplicate local-variable name: x
+TypeTests.dfy(72,6): Error: Duplicate local-variable name: y
+14 resolution/type errors detected in TypeTests.dfy
-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,7): Error: RHS expression must be well defined
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index fe8644be..ccdbcb91 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -55,3 +55,20 @@ class ArrayTests { a[7] := 13; // error: array elements are not ghost locations
}
}
+
+// ---------------------
+
+method DuplicateVarName(x: int) returns (y: int)
+{
+ var z: int;
+ var z: int; // error: redeclaration of local
+ var x := x; // redeclaration of in-parameter is fine
+ var x := x; // error: but a redeclaration of that local is not fine
+ {
+ var x := x; // an inner local variable of the same name is fine
+ var x := x; // error: but a redeclaration thereof is not okay
+ var y := y; // duplicating an out-parameter here is fine
+ }
+ var y := y; // error: redeclaration of an out-parameter is not allowed (it is
+ // treated like an outermost-scoped local in this regard)
+}
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index 20f4477b..75561d65 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -31,7 +31,7 @@ `(,(dafny-regexp-opt '(
"class" "datatype" "function" "frame" "ghost" "var" "method" "unlimited"
- "module" "imports" "static"
+ "module" "imports" "static" "refines" "replaces" "by"
"returns" "requires" "ensures" "modifies" "reads" "free"
"invariant" "decreases"
)) . font-lock-builtin-face)
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index dd44665a..5551cec0 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -7,13 +7,13 @@ \lstdefinelanguage{dafny}{
morekeywords={class,datatype,bool,int,object,set,seq,array,%
function,unlimited,
- ghost,var,static,
+ ghost,var,static,refines,replaces,by,
method,returns,module,imports,in,
requires,modifies,ensures,reads,decreases,free,
% expressions
match,case,false,true,null,old,fresh,this,
% statements
- assert,assume,print,new,havoc,call,if,then,else,while,invariant,break,return,foreach,
+ assert,assume,print,new,havoc,call,if,then,else,while,invariant,break,label,return,foreach,
},
literate=%
{:}{$\colon$}1
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim index 34379f6b..a6bccaa4 100644 --- a/Util/vim/syntax/dafny.vim +++ b/Util/vim/syntax/dafny.vim @@ -8,9 +8,9 @@ syntax case match syntax keyword dafnyFunction function method syntax keyword dafnyTypeDef class datatype syntax keyword dafnyConditional if then else match case -syntax keyword dafnyRepeat for while -syntax keyword dafnyStatement havoc assume assert return call new -syntax keyword dafnyKeyword var ghost returns null static this +syntax keyword dafnyRepeat foreach while +syntax keyword dafnyStatement havoc assume assert return call new print break label +syntax keyword dafnyKeyword var ghost returns null static this refines replaces by syntax keyword dafnyType int bool seq set syntax keyword dafnyLogic requires ensures modifies reads decreases invariant syntax keyword dafnyOperator forall exists old fresh |