diff options
| -rw-r--r-- | Dafny/Resolver.cs | 35 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 5 | ||||
| -rw-r--r-- | Test/dafny0/LiberalEquality.dfy | 55 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 | ||||
| -rw-r--r-- | Test/vacid0/LazyInitArray.dfy | 6 |
5 files changed, 97 insertions, 6 deletions
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index 3ff0c12b..3780e0d9 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -2889,8 +2889,10 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Eq:
case BinaryExpr.Opcode.Neq:
- if (!UnifyTypes(e.E0.Type, e.E1.Type)) {
- Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);
+ if (!CouldPossiblyBeSameType(e.E0.Type, e.E1.Type)) {
+ if (!UnifyTypes(e.E0.Type, e.E1.Type)) {
+ Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);
+ }
}
expr.Type = Type.Bool;
break;
@@ -3282,6 +3284,35 @@ namespace Microsoft.Dafny { }
}
+ private bool CouldPossiblyBeSameType(Type A, Type B) {
+ if (A.IsTypeParameter || B.IsTypeParameter) {
+ return true;
+ }
+ if (A.IsArrayType && B.IsArrayType) {
+ Type a = UserDefinedType.ArrayElementType(A);
+ Type b = UserDefinedType.ArrayElementType(B);
+ return CouldPossiblyBeSameType(a, b);
+ }
+ if (A is UserDefinedType && B is UserDefinedType) {
+ UserDefinedType a = (UserDefinedType)A;
+ UserDefinedType b = (UserDefinedType)B;
+ if (a.ResolvedClass != null && b.ResolvedClass != null && a.ResolvedClass == b.ResolvedClass) {
+ if (a.TypeArgs.Count != b.TypeArgs.Count) {
+ return false; // this probably doesn't happen if the classes are the same.
+ }
+ for (int i = 0; i < a.TypeArgs.Count; i++) {
+ if (!CouldPossiblyBeSameType(a.TypeArgs[i], b.TypeArgs[i]))
+ return false;
+ }
+ // all parameters could be the same
+ return true;
+ }
+ // either we don't know what class it is yet, or the classes mismatch
+ return false;
+ }
+ return false;
+ }
+
/// <summary>
/// Generate an error for every non-ghost feature used in "expr".
/// Requires "expr" to have been successfully resolved.
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 4edec058..a64cf3f3 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1576,6 +1576,11 @@ Execution trace: Dafny program verifier finished with 30 verified, 2 errors
+-------------------- LiberalEquality.dfy --------------------
+LiberalEquality.dfy(37,14): Error: arguments must have the same type (got Weird<T,int,V> and Weird<T,bool,V>)
+LiberalEquality.dfy(52,14): Error: arguments must have the same type (got array<int> and array<bool>)
+2 resolution/type errors detected in LiberalEquality.dfy
+
-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,11): Error: index out of range
Execution trace:
diff --git a/Test/dafny0/LiberalEquality.dfy b/Test/dafny0/LiberalEquality.dfy new file mode 100644 index 00000000..3dc52c80 --- /dev/null +++ b/Test/dafny0/LiberalEquality.dfy @@ -0,0 +1,55 @@ +
+class Array<T>
+{
+ var Length: nat;
+}
+
+class Test<T> {
+ var a: Array<int>;
+ var b: Array<T>;
+ predicate valid()
+ reads this, a, b;
+ {
+ a != null && b != null && a != b && a.Length == b.Length
+ }
+}
+
+method m1<T, U>(t: T, u: U)
+ requires t != u;
+{
+
+}
+
+method m2<T>(t: array<T>, a: array<int>)
+ requires t != null && a != null && t != a && t.Length == a.Length;
+{
+
+}
+
+
+class Weird<T, U, V>
+{
+
+}
+
+
+method m3<T, V>(a: Weird<T, int, V>, b: Weird<T, bool, V>)
+ requires a == b; // Bad: second parameter can't be both bool and int.
+{
+
+}
+
+
+method m4<T, U, V>(a: Weird<T, U, V>, b: Weird<T, bool, V>)
+ requires a == b;
+{
+
+}
+
+
+// Just to make sure nothing went wrong.
+method m5(a: array<int>, b: array<bool>)
+ requires a == b; // Bad: never equal
+{
+
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index e4c134f6..0da7fe3e 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -22,7 +22,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy LoopModifies.dfy Refinement.dfy RefinementErrors.dfy
ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
- Predicates.dfy Skeletons.dfy Maps.dfy) do (
+ Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy index e56a8317..3e5a95ef 100644 --- a/Test/vacid0/LazyInitArray.dfy +++ b/Test/vacid0/LazyInitArray.dfy @@ -11,10 +11,10 @@ class LazyInitArray<T> { reads this, a, b, c;
{
a != null && b != null && c != null &&
- a.Length == |Contents| + 1 && // TODO: remove the "+ 1" hack, which currently serves the purpose of distinguishing 'a' from 'b' and 'c'
+ a.Length == |Contents| &&
b.Length == |Contents| &&
c.Length == |Contents| &&
- b != c &&
+ b != c && a != b && a != c &&
0 <= n && n <= c.Length &&
(forall i :: 0 <= i && i < |Contents| ==>
Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else Zero)) &&
@@ -41,7 +41,7 @@ class LazyInitArray<T> { ensures |Contents| == N && Zero == zero;
ensures (forall x :: x in Contents ==> x == zero);
{
- a := new T[N+1];
+ a := new T[N];
b := new int[N];
c := new int[N];
n := 0;
|