diff options
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 64a23393..ff658378 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -64,7 +64,7 @@ void ObjectInvariant() public void ResolveProgram(Program prog) {
Contract.Requires(prog != null);
// register modules
- Dictionary<string,ModuleDecl> modules = new Dictionary<string,ModuleDecl>(); + Dictionary<string,ModuleDecl> modules = new Dictionary<string,ModuleDecl>();
foreach (ModuleDecl m in prog.Modules) {
if (modules.ContainsKey(m.Name)) {
Error(m, "Duplicate module name: {0}", m.Name);
@@ -116,12 +116,12 @@ void ObjectInvariant() foreach (TopLevelDecl decl in m.TopLevelDecls)
if (decl is ClassRefinementDecl) {
ClassRefinementDecl rdecl = (ClassRefinementDecl) decl;
- ResolveTopLevelRefinement(rdecl); + ResolveTopLevelRefinement(rdecl);
if (rdecl.Refined != null) refines.AddEdge(rdecl, rdecl.Refined);
}
// attempt finding refinement cycles
- List<TopLevelDecl> refinesCycle = refines.TryFindCycle(); + List<TopLevelDecl> refinesCycle = refines.TryFindCycle();
if (refinesCycle != null) {
string cy = "";
string sep = "";
@@ -293,7 +293,7 @@ void ObjectInvariant() } else if (member is CouplingInvariant) {
CouplingInvariant inv = (CouplingInvariant)member;
if (currentClass is ClassRefinementDecl) {
- ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined; + ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;
if (refined != null) {
Contract.Assert( classMembers.ContainsKey(refined));
Dictionary<string,MemberDecl> members = classMembers[refined];
@@ -302,13 +302,13 @@ void ObjectInvariant() List<Field> fields = new List<Field>();
foreach (IToken tok in inv.Toks) {
if (!members.ContainsKey(tok.val))
- Error(tok, "Refined class does not declare a field: {0}", tok.val); + Error(tok, "Refined class does not declare a field: {0}", tok.val);
else {
MemberDecl field = members[tok.val];
if (!(field is Field))
Error(tok, "Coupling invariant refers to a non-field member: {0}", tok.val);
else if (fields.Contains(cce.NonNull((Field)field)))
- Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val); + Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val);
else
fields.Add(cce.NonNull((Field)field));
}
@@ -324,9 +324,9 @@ void ObjectInvariant() }
if (currentClass is ClassRefinementDecl) {
- ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined; + ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;
if (refined != null) {
- Contract.Assert( classMembers.ContainsKey(refined)); + Contract.Assert( classMembers.ContainsKey(refined));
// there is a member with the same name in refined class if and only if the member is a refined method
if ((member is MethodRefinement) != (classMembers[refined].ContainsKey(member.Name)))
@@ -379,7 +379,7 @@ void ObjectInvariant() if (mf.Ins.Count != mf.Refined.Ins.Count)
Error(mf, "Different number of input variables");
if (mf.Outs.Count != mf.Refined.Outs.Count)
- Error(mf, "Different number of output variables"); + Error(mf, "Different number of output variables");
if (mf.IsStatic || mf.Refined.IsStatic)
Error(mf, "Refined methods cannot be static");
} else {
@@ -387,7 +387,7 @@ void ObjectInvariant() }
}
} else {
- Error(member, "Refinement methods can only be declared in refinement classes: {0}", member.Name); + Error(member, "Refinement methods can only be declared in refinement classes: {0}", member.Name);
}
}
@@ -1783,7 +1783,7 @@ void ObjectInvariant() ResolveExpression(ee, twoState, specContext);
Contract.Assert( ee.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(elementType, ee.Type)) {
- Error(ee, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", ee.Type, elementType); + Error(ee, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", ee.Type, elementType);
}
}
if (expr is SetDisplayExpr) {
|