From 129744b09404197d1f84481601edd51d0d104bd4 Mon Sep 17 00:00:00 2001
From: Reza Ahmadi <reza.ahmadi@uta.fi>
Date: Sun, 20 Jul 2014 19:09:18 +0300
Subject: - 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
---
 Test/dafny0/Trait/TraitOverride3.dfy               | 16 +++++++-
 Test/dafny0/Trait/TraitOverride3.dfy.expect        |  2 +-
 Test/dafny0/Trait/TraitUsingParentMembers.dfy      | 44 ++++++++++++++++++++++
 .../Trait/TraitUsingParentMembers.dfy.expect       |  8 ++++
 4 files changed, 67 insertions(+), 3 deletions(-)
 create mode 100644 Test/dafny0/Trait/TraitUsingParentMembers.dfy
 create mode 100644 Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect

(limited to 'Test/dafny0')

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
-- 
cgit v1.2.3