diff options
| author |  leino <unknown> | 2014-08-13 07:24:33 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-08-13 07:24:33 -0700 |
| commit | 2a6bd63460d27db7fc11f7b99e231f4f587b6a70 (patch) | |
| tree | 26d89193bc29b6c469eb41a8f88b531e4f7c9513 | |
| parent | 9f24fd54271e0e70aba494905416f58ff0348c7c (diff) | |
Re-included lost calls to CheckEqualityTypes_Type
Modified syntax in some tests, since predicates now require parentheses (without parentheses refers to a predicate, not an application of the predicate)
| -rw-r--r-- | Source/Dafny/Resolver.cs | 15 | ||||
| -rw-r--r-- | Test/dafny0/snapshots/Snapshots1.v0.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny0/snapshots/Snapshots1.v1.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny0/snapshots/Snapshots2.v0.dfy | 12 | ||||
| -rw-r--r-- | Test/dafny0/snapshots/Snapshots2.v1.dfy | 12 |
5 files changed, 22 insertions, 25 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 341bfd67..568fe224 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1732,7 +1732,7 @@ namespace Microsoft.Dafny var iter = (IteratorDecl)d;
foreach (var p in iter.Ins) {
if (!p.IsGhost) {
- // CheckEqualityTypes_Type(p.tok, p.Type);
+ CheckEqualityTypes_Type(p.tok, p.Type);
}
}
foreach (var p in iter.Outs) {
@@ -1749,18 +1749,15 @@ namespace Microsoft.Dafny if (!member.IsGhost) {
if (member is Field) {
var f = (Field)member;
- // CheckEqualityTypes_Type(f.tok, f.Type);
- // Why check this?!
+ CheckEqualityTypes_Type(f.tok, f.Type);
} else if (member is Function) {
var f = (Function)member;
foreach (var p in f.Formals) {
if (!p.IsGhost) {
- // CheckEqualityTypes_Type(p.tok, p.Type);
- // Why check this?!
+ CheckEqualityTypes_Type(p.tok, p.Type);
}
}
- // CheckEqualityTypes_Type(f.tok, f.ResultType);
- // Why should we check this?!
+ CheckEqualityTypes_Type(f.tok, f.ResultType);
if (f.Body != null) {
CheckEqualityTypes(f.Body);
}
@@ -1768,12 +1765,12 @@ namespace Microsoft.Dafny var m = (Method)member;
foreach (var p in m.Ins) {
if (!p.IsGhost) {
- // CheckEqualityTypes_Type(p.tok, p.Type);
+ CheckEqualityTypes_Type(p.tok, p.Type);
}
}
foreach (var p in m.Outs) {
if (!p.IsGhost) {
- // CheckEqualityTypes_Type(p.tok, p.Type);
+ CheckEqualityTypes_Type(p.tok, p.Type);
}
}
if (m.Body != null) {
diff --git a/Test/dafny0/snapshots/Snapshots1.v0.dfy b/Test/dafny0/snapshots/Snapshots1.v0.dfy index dd1e7deb..34d066c3 100644 --- a/Test/dafny0/snapshots/Snapshots1.v0.dfy +++ b/Test/dafny0/snapshots/Snapshots1.v0.dfy @@ -5,9 +5,9 @@ method M() }
method N()
- ensures P;
+ ensures P();
-predicate P
+predicate P()
{
false
}
diff --git a/Test/dafny0/snapshots/Snapshots1.v1.dfy b/Test/dafny0/snapshots/Snapshots1.v1.dfy index 93ad6068..184ac65d 100644 --- a/Test/dafny0/snapshots/Snapshots1.v1.dfy +++ b/Test/dafny0/snapshots/Snapshots1.v1.dfy @@ -5,9 +5,9 @@ method M() }
method N()
- ensures P;
+ ensures P();
-predicate P
+predicate P()
{
true
}
diff --git a/Test/dafny0/snapshots/Snapshots2.v0.dfy b/Test/dafny0/snapshots/Snapshots2.v0.dfy index 37b9982b..727e177d 100644 --- a/Test/dafny0/snapshots/Snapshots2.v0.dfy +++ b/Test/dafny0/snapshots/Snapshots2.v0.dfy @@ -5,15 +5,15 @@ method M() }
method N()
- ensures P;
+ ensures P();
-predicate P
- ensures P == Q;
+predicate P()
+ ensures P() == Q();
-predicate Q
- ensures Q == R;
+predicate Q()
+ ensures Q() == R();
-predicate R
+predicate R()
{
false
}
diff --git a/Test/dafny0/snapshots/Snapshots2.v1.dfy b/Test/dafny0/snapshots/Snapshots2.v1.dfy index 03719744..02a91b52 100644 --- a/Test/dafny0/snapshots/Snapshots2.v1.dfy +++ b/Test/dafny0/snapshots/Snapshots2.v1.dfy @@ -5,15 +5,15 @@ method M() }
method N()
- ensures P;
+ ensures P();
-predicate P
- ensures P == Q;
+predicate P()
+ ensures P() == Q();
-predicate Q
- ensures Q == R;
+predicate Q()
+ ensures Q() == R();
-predicate R
+predicate R()
{
true
}
|