summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Reza Ahmadi <reza.ahmadi@uta.fi>2014-07-20 19:09:18 +0300
committerGravatar Reza Ahmadi <reza.ahmadi@uta.fi>2014-07-20 19:09:18 +0300
commit129744b09404197d1f84481601edd51d0d104bd4 (patch)
treee46b8fd4cf3f428127cee279cb334fa9b3d4dc05 /Source
parent2c9d68a529b04dcb1c18025306713644a602833c (diff)
- fixed a bug in inheriting members from a trait
=> ResolvedClass in userdefinedtypes used to be null-> fixed - checking only bodyless methods and functions to make sure they have been implemented in the child class - added one more test
Diffstat (limited to 'Source')
-rw-r--r--Source/Dafny/Cloner.cs7
-rw-r--r--Source/Dafny/Resolver.cs40
2 files changed, 28 insertions, 19 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 5dfc67d5..b462f983 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -137,8 +137,6 @@ namespace Microsoft.Dafny
var f = (Field)member;
Field field = new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, f.IsUserMutable, CloneType(f.Type), CloneAttributes(f.Attributes));
field.Inherited = member.Inherited; //we do need this information in ResolveClassMemberTypes method
- if (field.Type is UserDefinedType)
- ((UserDefinedType)field.Type).ResolvedClass = ((UserDefinedType)(((Field)(member)).Type)).ResolvedClass;
return field;
} else if (member is Function) {
var f = (Function)member;
@@ -184,7 +182,10 @@ namespace Microsoft.Dafny
}
public Formal CloneFormal(Formal formal) {
- return new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost);
+ Formal f = new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost);
+ if (f.Type is UserDefinedType && formal.Type is UserDefinedType)
+ ((UserDefinedType)f.Type).ResolvedClass = ((UserDefinedType)(formal.Type)).ResolvedClass;
+ return f;
}
public BoundVar CloneBoundVar(BoundVar bv) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index d503076c..9798e79f 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2916,13 +2916,16 @@ namespace Microsoft.Dafny
else //the member is not already in the class
{
MemberDecl classNewMember = cloner.CloneMember(traitMem.Value);
+ if (classNewMember is Field)
+ {
+ Field f = (Field)classNewMember;
+ if (f.Type is UserDefinedType)
+ ((UserDefinedType)f.Type).ResolvedClass = ((UserDefinedType)(((Field)(traitMem.Value)).Type)).ResolvedClass;
+ }
classNewMember.EnclosingClass = cl;
classNewMember.Inherited = true;
classMembers[cl].Add(traitMem.Key, classNewMember);
cl.Members.Add(classNewMember);
- //traitMem.Value.Inherited = true;
- //classMembers[cl].Add(traitMem.Key, traitMem.Value);
- //cl.Members.Add(traitMem.Value);
}
}//foreach
@@ -2934,27 +2937,32 @@ namespace Microsoft.Dafny
if (traitMember is Function)
{
Function traitFunc = (Function)traitMember;
- var classMem = cl.Members.Where(clMem => clMem is Function).FirstOrDefault(clMem => ((Function)clMem).Body != null && clMem.CompileName == traitMember.CompileName);
- if (classMem != null)
+ if (traitFunc.Body == null) //we do this check only if trait function body is null
{
- Function classFunc = (Function)classMem;
- refinementTransformer.CheckOverride_FunctionParameters(classFunc, traitFunc);
+ var classMem = cl.Members.Where(clMem => clMem is Function).FirstOrDefault(clMem => ((Function)clMem).Body != null && clMem.CompileName == traitMember.CompileName);
+ if (classMem != null)
+ {
+ Function classFunc = (Function)classMem;
+ refinementTransformer.CheckOverride_FunctionParameters(classFunc, traitFunc);
+ }
+ else if (!cl.Module.IsAbstract && traitFunc.Body == null && classMem == null)
+ Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitFunc.CompileName);
}
- else if (!cl.Module.IsAbstract && traitFunc.Body == null && classMem == null)
- Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitFunc.CompileName);
}
if (traitMember is Method)
{
Method traitMethod = (Method)traitMember;
-
- var classMem = cl.Members.Where(clMem => clMem is Method).FirstOrDefault(clMem => ((Method)clMem).Body != null && clMem.CompileName == traitMember.CompileName);
- if (classMem != null)
+ if (traitMethod.Body == null) //we do this check only if trait method body is null
{
- Method classMethod = (Method)classMem;
- refinementTransformer.CheckOverride_MethodParameters(classMethod, traitMethod);
+ var classMem = cl.Members.Where(clMem => clMem is Method).FirstOrDefault(clMem => ((Method)clMem).Body != null && clMem.CompileName == traitMember.CompileName);
+ if (classMem != null)
+ {
+ Method classMethod = (Method)classMem;
+ refinementTransformer.CheckOverride_MethodParameters(classMethod, traitMethod);
+ }
+ if (!cl.Module.IsAbstract && traitMethod.Body == null && classMem == null)
+ Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitMethod.CompileName);
}
- if (!cl.Module.IsAbstract && traitMethod.Body == null && classMem == null)
- Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitMethod.CompileName);
}
}
}