diff options
| -rw-r--r-- | Test/dafny0/Answer | 221 | ||||
| -rw-r--r-- | Test/dafny0/Array.dfy | 18 | ||||
| -rw-r--r-- | Test/dafny0/Definedness.dfy | 16 | ||||
| -rw-r--r-- | Test/dafny0/NatTypes.dfy | 3 | ||||
| -rw-r--r-- | Test/dafny0/Termination.dfy | 5 | ||||
| -rw-r--r-- | Test/dafny0/TypeAntecedents.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny0/TypeParameters.dfy | 23 |
7 files changed, 169 insertions, 121 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index a6f1e9b7..d9294f1a 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -74,12 +74,14 @@ TypeTests.dfy(58,8): Error: Duplicate local-variable name: x TypeTests.dfy(61,6): Error: Duplicate local-variable name: y
TypeTests.dfy(68,17): Error: member F in type C does not refer to a method
TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments
-TypeTests.dfy(78,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
-TypeTests.dfy(79,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
+TypeTests.dfy(78,10): Error: cannot assign to multiple array elements (try a foreach).
+TypeTests.dfy(78,10): Error: cannot assign to multiple array elements (try a foreach).
+TypeTests.dfy(79,10): Error: cannot assign to multiple array elements (try a foreach).
+TypeTests.dfy(79,10): Error: cannot assign to multiple array elements (try a foreach).
TypeTests.dfy(85,9): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(86,8): Error: sorry, cannot instantiate 'array' type with a subrange type
TypeTests.dfy(87,8): Error: sorry, cannot instantiate 'array' type with a subrange type
-21 resolution/type errors detected in TypeTests.dfy
+23 resolution/type errors detected in TypeTests.dfy
-------------------- NatTypes.dfy --------------------
NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative
@@ -102,20 +104,20 @@ NatTypes.dfy(40,14): Error: assertion violation Execution trace:
(0,0): anon0
(0,0): anon4_Then
-NatTypes.dfy(54,16): Error: assertion violation
+NatTypes.dfy(57,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-NatTypes.dfy(68,16): Error: assertion violation
+NatTypes.dfy(71,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
-NatTypes.dfy(86,19): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(89,19): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-NatTypes.dfy(101,45): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(104,45): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon6_Else
(0,0): anon7_Else
@@ -231,149 +233,167 @@ Execution trace: Definedness.dfy(50,18): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(55,18): Error: target object may be null
+Definedness.dfy(51,3): Error BP5003: A postcondition might not hold on this return path.
+Definedness.dfy(50,22): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Definedness.dfy(77,7): Error: target object may be null
+Definedness.dfy(57,18): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(78,5): Error: possible violation of function precondition
+Definedness.dfy(58,3): Error BP5003: A postcondition might not hold on this return path.
+Definedness.dfy(57,22): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Definedness.dfy(79,10): Error: possible violation of function precondition
+Definedness.dfy(65,3): Error BP5003: A postcondition might not hold on this return path.
+Definedness.dfy(64,22): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Definedness.dfy(84,14): Error: possible division by zero
+Definedness.dfy(85,7): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(84,23): Error: possible division by zero
+Definedness.dfy(86,5): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Definedness.dfy(85,15): Error: possible division by zero
+Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
-Definedness.dfy(90,12): Error: possible division by zero
+Definedness.dfy(86,10): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(97,15): Error: possible division by zero
+Definedness.dfy(87,10): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
- Definedness.dfy(97,5): anon8_LoopHead
+Definedness.dfy(92,14): Error: possible division by zero
+Execution trace:
+ (0,0): anon0
+Definedness.dfy(92,23): Error: possible division by zero
+Execution trace:
+ (0,0): anon0
+Definedness.dfy(93,15): Error: possible division by zero
+Execution trace:
+ (0,0): anon0
+Definedness.dfy(98,12): Error: possible division by zero
+Execution trace:
+ (0,0): anon0
+Definedness.dfy(105,15): Error: possible division by zero
+Execution trace:
+ (0,0): anon0
+ Definedness.dfy(105,5): anon8_LoopHead
(0,0): anon8_LoopBody
- Definedness.dfy(97,5): anon9_Else
+ Definedness.dfy(105,5): anon9_Else
(0,0): anon3
-Definedness.dfy(106,23): Error: possible violation of function precondition
+Definedness.dfy(114,23): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
- Definedness.dfy(105,5): anon13_LoopHead
+ Definedness.dfy(113,5): anon13_LoopHead
(0,0): anon13_LoopBody
(0,0): anon14_Then
-Definedness.dfy(112,17): Error: possible violation of function precondition
+Definedness.dfy(120,17): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
- Definedness.dfy(105,5): anon13_LoopHead
+ Definedness.dfy(113,5): anon13_LoopHead
(0,0): anon13_LoopBody
- Definedness.dfy(105,5): anon14_Else
+ Definedness.dfy(113,5): anon14_Else
(0,0): anon3
(0,0): anon15_Then
(0,0): anon6
- Definedness.dfy(111,5): anon16_LoopHead
+ Definedness.dfy(119,5): anon16_LoopHead
(0,0): anon16_LoopBody
(0,0): anon17_Then
-Definedness.dfy(122,17): Error: possible violation of function precondition
+Definedness.dfy(130,17): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
- Definedness.dfy(121,5): anon7_LoopHead
+ Definedness.dfy(129,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-Definedness.dfy(122,22): Error BP5004: This loop invariant might not hold on entry.
+Definedness.dfy(130,22): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
-Definedness.dfy(123,17): Error: possible violation of function precondition
+Definedness.dfy(131,17): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
- Definedness.dfy(121,5): anon7_LoopHead
+ Definedness.dfy(129,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-Definedness.dfy(132,15): Error: possible division by zero
+Definedness.dfy(140,15): Error: possible division by zero
Execution trace:
(0,0): anon0
- Definedness.dfy(132,5): anon9_LoopHead
+ Definedness.dfy(140,5): anon9_LoopHead
(0,0): anon9_LoopBody
- Definedness.dfy(132,5): anon10_Else
+ Definedness.dfy(140,5): anon10_Else
(0,0): anon3
-Definedness.dfy(151,15): Error: possible division by zero
+Definedness.dfy(159,15): Error: possible division by zero
Execution trace:
(0,0): anon0
- Definedness.dfy(145,5): anon17_LoopHead
+ Definedness.dfy(153,5): anon17_LoopHead
(0,0): anon17_LoopBody
- Definedness.dfy(145,5): anon18_Else
+ Definedness.dfy(153,5): anon18_Else
(0,0): anon3
(0,0): anon19_Then
(0,0): anon5
(0,0): anon20_Then
(0,0): anon8
- Definedness.dfy(151,5): anon21_LoopHead
+ Definedness.dfy(159,5): anon21_LoopHead
(0,0): anon21_LoopBody
- Definedness.dfy(151,5): anon22_Else
+ Definedness.dfy(159,5): anon22_Else
(0,0): anon11
-Definedness.dfy(170,17): Error: possible violation of function precondition
+Definedness.dfy(172,28): Error BP5004: This loop invariant might not hold on entry.
+Execution trace:
+ (0,0): anon0
+Definedness.dfy(178,17): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
- Definedness.dfy(162,5): anon19_LoopHead
+ Definedness.dfy(170,5): anon19_LoopHead
(0,0): anon19_LoopBody
- Definedness.dfy(162,5): anon20_Else
+ Definedness.dfy(170,5): anon20_Else
(0,0): anon3
(0,0): anon21_Then
(0,0): anon6
- Definedness.dfy(169,5): anon22_LoopHead
+ Definedness.dfy(177,5): anon22_LoopHead
(0,0): anon22_LoopBody
(0,0): anon23_Then
(0,0): anon24_Then
(0,0): anon11
-Definedness.dfy(191,24): Error: possible violation of function precondition
+Definedness.dfy(199,24): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Definedness.dfy(193,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
+Definedness.dfy(201,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
Execution trace:
(0,0): anon0
-Definedness.dfy(195,33): Error: range expression must be well defined
+Definedness.dfy(203,33): Error: range expression must be well defined
Execution trace:
(0,0): anon0
-Definedness.dfy(201,18): Error: RHS of assignment must be well defined
+Definedness.dfy(218,19): Error: possible division by zero
Execution trace:
(0,0): anon0
-Definedness.dfy(210,19): Error: possible division by zero
-Execution trace:
- (0,0): anon0
- Definedness.dfy(208,5): anon7_LoopHead
+ Definedness.dfy(216,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-Definedness.dfy(210,23): Error BP5004: This loop invariant might not hold on entry.
+Definedness.dfy(218,23): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
-Definedness.dfy(210,28): Error: possible division by zero
+Definedness.dfy(218,28): Error: possible division by zero
Execution trace:
(0,0): anon0
- Definedness.dfy(208,5): anon7_LoopHead
+ Definedness.dfy(216,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-Definedness.dfy(231,46): Error: possible violation of function postcondition
+Definedness.dfy(239,46): Error: possible violation of function postcondition
Execution trace:
(0,0): anon0
(0,0): anon5_Else
-Definedness.dfy(238,22): Error: target object may be null
+Definedness.dfy(246,22): Error: target object may be null
Execution trace:
(0,0): anon5_Then
(0,0): anon2
(0,0): anon6_Then
-Definedness.dfy(254,24): Error: possible violation of function postcondition
+Definedness.dfy(262,24): Error: possible violation of function postcondition
Execution trace:
(0,0): anon7_Then
(0,0): anon2
(0,0): anon8_Else
-Dafny program verifier finished with 23 verified, 34 errors
+Dafny program verifier finished with 23 verified, 39 errors
-------------------- FunctionSpecifications.dfy --------------------
FunctionSpecifications.dfy(28,13): Error: possible violation of function postcondition
@@ -484,27 +504,24 @@ Execution trace: (0,0): anon5_Then
(0,0): anon2
(0,0): anon6_Then
-Array.dfy(95,18): Error: assertion violation
-Execution trace:
- (0,0): anon0
-Array.dfy(110,6): Error: insufficient reads clause to read array element
+Array.dfy(97,6): Error: insufficient reads clause to read array element
Execution trace:
(0,0): anon7_Else
(0,0): anon8_Then
(0,0): anon9_Then
-Array.dfy(118,6): Error: insufficient reads clause to read array element
+Array.dfy(105,6): Error: insufficient reads clause to read array element
Execution trace:
(0,0): anon7_Else
(0,0): anon8_Then
(0,0): anon9_Then
-Array.dfy(134,6): Error: assignment may update an array element not in the enclosing context's modifies clause
+Array.dfy(121,6): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
-Array.dfy(141,6): Error: assignment may update an array element not in the enclosing context's modifies clause
+Array.dfy(128,6): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 22 verified, 11 errors
+Dafny program verifier finished with 21 verified, 10 errors
-------------------- MultiDimArray.dfy --------------------
MultiDimArray.dfy(53,21): Error: assertion violation
@@ -812,61 +829,61 @@ Execution trace: Dafny program verifier finished with 18 verified, 10 errors
-------------------- Termination.dfy --------------------
-Termination.dfy(100,3): Error: cannot prove termination; try supplying a decreases clause for the loop
+Termination.dfy(105,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
(0,0): anon0
- Termination.dfy(100,3): anon7_LoopHead
+ Termination.dfy(105,3): anon7_LoopHead
(0,0): anon7_LoopBody
- Termination.dfy(100,3): anon8_Else
+ Termination.dfy(105,3): anon8_Else
(0,0): anon3
- Termination.dfy(100,3): anon9_Else
+ Termination.dfy(105,3): anon9_Else
(0,0): anon5
-Termination.dfy(108,3): Error: cannot prove termination; try supplying a decreases clause for the loop
+Termination.dfy(113,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
(0,0): anon0
- Termination.dfy(108,3): anon9_LoopHead
+ Termination.dfy(113,3): anon9_LoopHead
(0,0): anon9_LoopBody
- Termination.dfy(108,3): anon10_Else
+ Termination.dfy(113,3): anon10_Else
(0,0): anon11_Then
(0,0): anon5
- Termination.dfy(108,3): anon12_Else
+ Termination.dfy(113,3): anon12_Else
(0,0): anon7
-Termination.dfy(117,3): Error: decreases expression might not decrease
+Termination.dfy(122,3): Error: decreases expression might not decrease
Execution trace:
(0,0): anon0
- Termination.dfy(117,3): anon9_LoopHead
+ Termination.dfy(122,3): anon9_LoopHead
(0,0): anon9_LoopBody
- Termination.dfy(117,3): anon10_Else
+ Termination.dfy(122,3): anon10_Else
(0,0): anon11_Then
(0,0): anon5
- Termination.dfy(117,3): anon12_Else
+ Termination.dfy(122,3): anon12_Else
(0,0): anon7
-Termination.dfy(118,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
+Termination.dfy(123,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
Execution trace:
(0,0): anon0
- Termination.dfy(117,3): anon9_LoopHead
+ Termination.dfy(122,3): anon9_LoopHead
(0,0): anon9_LoopBody
- Termination.dfy(117,3): anon10_Else
+ Termination.dfy(122,3): anon10_Else
(0,0): anon11_Then
(0,0): anon5
- Termination.dfy(117,3): anon12_Else
+ Termination.dfy(122,3): anon12_Else
(0,0): anon7
-Termination.dfy(246,35): Error: cannot prove termination; try supplying a decreases clause
+Termination.dfy(251,35): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
-Termination.dfy(286,3): Error: decreases expression might not decrease
+Termination.dfy(291,3): Error: decreases expression might not decrease
Execution trace:
(0,0): anon0
- Termination.dfy(286,3): anon10_LoopHead
+ Termination.dfy(291,3): anon10_LoopHead
(0,0): anon10_LoopBody
- Termination.dfy(286,3): anon11_Else
- Termination.dfy(286,3): anon12_Else
+ Termination.dfy(291,3): anon11_Else
+ Termination.dfy(291,3): anon12_Else
(0,0): anon13_Else
(0,0): anon8
-Dafny program verifier finished with 44 verified, 6 errors
+Dafny program verifier finished with 45 verified, 6 errors
-------------------- DTypes.dfy --------------------
DTypes.dfy(15,14): Error: assertion violation
@@ -898,46 +915,46 @@ Execution trace: Dafny program verifier finished with 27 verified, 6 errors
-------------------- TypeParameters.dfy --------------------
-TypeParameters.dfy(41,22): Error: assertion violation
+TypeParameters.dfy(44,22): Error: assertion violation
Execution trace:
(0,0): anon0
-TypeParameters.dfy(63,27): Error: assertion violation
+TypeParameters.dfy(66,27): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
(0,0): anon2
-TypeParameters.dfy(130,12): Error: assertion violation
-TypeParameters.dfy(130,28): Related location: Related location
+TypeParameters.dfy(138,12): Error: assertion violation
+TypeParameters.dfy(138,28): Related location: Related location
Execution trace:
(0,0): anon0
(0,0): anon14_Then
- TypeParameters.dfy(130,32): anon15_Else
+ TypeParameters.dfy(138,32): anon15_Else
(0,0): anon5
-TypeParameters.dfy(132,12): Error: assertion violation
-TypeParameters.dfy(132,33): Related location: Related location
+TypeParameters.dfy(140,12): Error: assertion violation
+TypeParameters.dfy(140,33): Related location: Related location
Execution trace:
(0,0): anon0
(0,0): anon17_Then
- TypeParameters.dfy(132,37): anon18_Else
+ TypeParameters.dfy(140,37): anon18_Else
(0,0): anon11
-TypeParameters.dfy(146,15): Error BP5005: This loop invariant might not be maintained by the loop.
-TypeParameters.dfy(146,38): Related location: Related location
+TypeParameters.dfy(154,15): Error BP5005: This loop invariant might not be maintained by the loop.
+TypeParameters.dfy(154,38): Related location: Related location
Execution trace:
(0,0): anon0
- TypeParameters.dfy(139,3): anon17_LoopHead
+ TypeParameters.dfy(147,3): anon17_LoopHead
(0,0): anon17_LoopBody
- TypeParameters.dfy(139,3): anon18_Else
+ TypeParameters.dfy(147,3): anon18_Else
(0,0): anon5
(0,0): anon20_Then
(0,0): anon8
- TypeParameters.dfy(145,3): anon21_LoopHead
+ TypeParameters.dfy(153,3): anon21_LoopHead
(0,0): anon21_LoopBody
- TypeParameters.dfy(145,3): anon22_Else
+ TypeParameters.dfy(153,3): anon22_Else
(0,0): anon13
- TypeParameters.dfy(145,3): anon24_Else
+ TypeParameters.dfy(153,3): anon24_Else
(0,0): anon15
-Dafny program verifier finished with 33 verified, 5 errors
+Dafny program verifier finished with 35 verified, 5 errors
-------------------- Datatypes.dfy --------------------
Datatypes.dfy(79,20): Error: assertion violation
diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy index 1a18be6d..f667e699 100644 --- a/Test/dafny0/Array.dfy +++ b/Test/dafny0/Array.dfy @@ -73,16 +73,16 @@ class A { method Q() {
var a := new int[5];
- y[0],y[1],y[2],y[3],y[4] := 0,1,2,3,4;
+ a[0],a[1],a[2],a[3],a[4] := 0,1,2,3,4;
- assert [1,2,3,4] == y[1..];
- assert [1,2,3,4] == y[1.. y.Length];
- assert [1] == y[1..2];
- assert [0,1] == y[..2];
- assert [0,1] == y[0..2];
- assert forall i :: 0 <= i <= y.Length ==> [] == y[i..i];
- assert [0,1,2,3,4] == y[..];
- assert forall i :: 0 <= i < y.Length ==> y[i] == i;
+ assert [1,2,3,4] == a[1..];
+ assert [1,2,3,4] == a[1.. a.Length];
+ assert [1] == a[1..2];
+ assert [0,1] == a[..2];
+ assert [0,1] == a[0..2];
+ assert forall i :: 0 <= i <= a.Length ==> [] == a[i..i];
+ assert [0,1,2,3,4] == a[..];
+ assert forall i :: 0 <= i < a.Length ==> a[i] == i;
}
}
diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy index 2063eec4..44b54f3d 100644 --- a/Test/dafny0/Definedness.dfy +++ b/Test/dafny0/Definedness.dfy @@ -48,27 +48,35 @@ class SoWellformed { requires next != null;
modifies this;
ensures next.xyz < 100; // error: may not be well-defined (if body sets next to null)
+ {
+ }
method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed)
requires next != null;
modifies s;
ensures next.xyz < 100; // error: may not be well-defined (if this in s and body sets next to null)
-
+ {
+
+ }
method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed)
requires next != null && this !in s;
modifies s;
ensures next.xyz < 100; // fine
+ {
+
+ }
}
// ---------------------- welldefinedness checks for statements -------------------
class StatementTwoShoes {
var x: int;
-
+ var s: StatementTwoShoes;
function method F(b: int): StatementTwoShoes
requires 0 <= b;
+ reads this;
{
- this
+ s
}
method M(p: StatementTwoShoes, a: int)
@@ -175,7 +183,7 @@ class StatementTwoShoes { }
function G(w: int): int { 5 }
- function method H(x: int): int
+ function method H(x: int): int { -x }
method V(s: set<StatementTwoShoes>, a: int, b: int)
modifies s;
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy index e56b4122..47bc22e1 100644 --- a/Test/dafny0/NatTypes.dfy +++ b/Test/dafny0/NatTypes.dfy @@ -43,6 +43,9 @@ method Generic<T>(i: int, t0: T, t1: T) returns (r: T) { }
function method FenEric<T>(t0: T, t1: T): T
+{
+ t1
+}
datatype Pair<T> = Pr(T, T);
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index f31935af..1482dc24 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -90,6 +90,11 @@ class Termination { method Traverse<T>(a: List<T>) returns (val: T, b: List<T>)
requires a != List.Nil;
ensures a == List.Cons(val, b);
+ {
+ match a {
+ case Cons(v, r) => val := v; b := r;
+ }
+ }
}
datatype List<T> = Nil | Cons(T, List<T>);
diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy index 710e9838..5982a9e6 100644 --- a/Test/dafny0/TypeAntecedents.dfy +++ b/Test/dafny0/TypeAntecedents.dfy @@ -87,8 +87,8 @@ method N() returns (k: MyClass) {
k := new MyClass;
}
-
-function NF(): MyClass
+var a: MyClass;
+function NF(): MyClass reads this; { a }
function TakesADatatype(a: List): int { 12 }
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index 8f3f8b87..d6804661 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -14,10 +14,13 @@ class C<U> { {
var t := F(3,u) && F(this,u);
var kz := M(t,u);
- assert kz && (G() || !G());
+ var a := G();
+ assert kz && (a || !a);
+ }
+ method G<Y>() returns (a: Y)
+ {
+
}
-
- function G<Y>(): Y
}
class SetTest {
@@ -101,6 +104,9 @@ class CClient { static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
requires c == c || c in people;
+{
+ false
+}
method FindCelebrity3(people: set<int>, ghost c: int)
requires IsCelebrity(c, people); // once upon a time, this caused the translator to produce bad Boogie
@@ -112,7 +118,9 @@ method FindCelebrity3(people: set<int>, ghost c: int) static function F(c: int, people: set<int>): bool
requires IsCelebrity(c, people);
-
+{
+ false
+}
function RogerThat<G>(g: G): G
{
g
@@ -154,7 +162,14 @@ method LoopyRoger(n: int) class TyKn_C<T> {
var x: T;
function G(): T
+ reads this;
+ {
+ x
+ }
method M() returns (t: T)
+ {
+
+ }
}
class TyKn_K {
|