diff options
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Trait/TraitOverride3.dfy | 16 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitOverride3.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitUsingParentMembers.dfy | 44 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect | 8 |
4 files changed, 67 insertions, 3 deletions
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
|