- 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

6 files changed, 95 insertions, 22 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);

                       }

                   }

               }

diff --git a/Test/dafny0/Trait/TraitOverride3.dfy b/Test/dafny0/Trait/TraitOverride3.dfy
index d602bffb..467ad333 100644
--- a/Test/dafny0/Trait/TraitOverride3.dfy
+++ b/Test/dafny0/Trait/TraitOverride3.dfy
@@ -2,8 +2,7 @@
 // RUN: %diff "%s.expect" "%t"

 

 

-//related compiler changes

-//everything works OK in the following code

+//everything should work OK in the following program

 trait J 

 {

 	function method F(y: int): int

@@ -45,3 +44,16 @@ class c extends t
      2

   }

 }

+

+trait P1

+{

+  method M(N: int, a: array<int>) returns (sum: int)

+  {

+    sum := 1;   

+  }

+}

+

+class C1 extends P1

+{

+

+}

diff --git a/Test/dafny0/Trait/TraitOverride3.dfy.expect b/Test/dafny0/Trait/TraitOverride3.dfy.expect
index 5f41963f..73727958 100644
--- a/Test/dafny0/Trait/TraitOverride3.dfy.expect
+++ b/Test/dafny0/Trait/TraitOverride3.dfy.expect
@@ -1,2 +1,2 @@
 

-Dafny program verifier finished with 17 verified, 0 errors

+Dafny program verifier finished with 21 verified, 0 errors

diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy b/Test/dafny0/Trait/TraitUsingParentMembers.dfy
new file mode 100644
index 00000000..dd45d0e6
--- /dev/null
+++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy
@@ -0,0 +1,44 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+

+trait P1

+{

+	method N0() {

+	    var a: array<int>;

+	    if (a != null && 5 < a.Length) {

+	      a[5] := 12;  // error: violates modifies clause

+	    }

+	}

+

+	method Mul(x: int, y: int) returns (r: int)

+	  requires 0 <= x && 0 <= y;

+	  ensures r == x*y;

+	  decreases x;

+}

+

+class C1 extends P1

+{

+    method Mul(x: int, y: int) returns (r: int)

+	  requires 0 <= x && 0 <= y;

+	  ensures r == x*y;

+	  decreases x;

+	{

+	  if (x == 0) {

+		r := 0;

+	  } else {

+		var m := Mul(x-1, y);

+		r := m + y;

+	  }

+	}

+

+   method Testing(arr:array<int>)

+     requires arr != null && arr.Length == 2 && arr[0]== 1 && arr[1] == 10;

+   {

+      N0(); //calling parent trait methods

+      var x := 2;

+      var y := 5;

+      var z := Mul(x,y);

+      assert (z == 10);

+   }   

+}
\ No newline at end of file
diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect
new file mode 100644
index 00000000..6849499c
--- /dev/null
+++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect
@@ -0,0 +1,8 @@
+TraitUsingParentMembers.dfy(10,9): Error: assignment may update an array element not in the enclosing context's modifies clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    (0,0): anon2

+    (0,0): anon6_Then

+

+Dafny program verifier finished with 9 verified, 1 error