diff options
| author |  Rustan Leino <unknown> | 2014-01-11 10:36:54 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-01-11 10:36:54 -0800 |
| commit | 59f0250f9b4cb78b65f48cfcbddfd22f5271e96d (patch) | |
| tree | 3b3072b7f5a58abaedce92282df62c3e96654b64 | |
| parent | ad2d0b62367ee8c99f1b037190b2c29c4b7434a5 (diff) | |
| parent | 335ac08951e427500de34d55b14713cced6c12bd (diff) | |
Merge
| -rw-r--r-- | Source/Dafny/Cloner.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 5 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 26 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/AutoReq.dfy | 13 |
5 files changed, 34 insertions, 14 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index fa6d635c..6a3052fe 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -201,7 +201,7 @@ namespace Microsoft.Dafny } else if (expr is LiteralExpr) {
var e = (LiteralExpr)expr;
if (e is StaticReceiverExpr) {
- return new StaticReceiverExpr(e.tok, e.Type);
+ return new StaticReceiverExpr(e.tok, CloneType(e.Type));
} else if (e.Value == null) {
return new LiteralExpr(Tok(e.tok));
} else if (e.Value is bool) {
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 5afac116..4d67dbe9 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -4174,11 +4174,13 @@ namespace Microsoft.Dafny { /// </summary>
public class StaticReceiverExpr : LiteralExpr
{
+ public readonly Type UnresolvedType;
+
public StaticReceiverExpr(IToken tok, Type t)
: base(tok) {
Contract.Requires(tok != null);
Contract.Requires(t != null);
- Type = t;
+ UnresolvedType = t;
}
public StaticReceiverExpr(IToken tok, ClassDecl cl)
@@ -4191,6 +4193,7 @@ namespace Microsoft.Dafny { typeArgs.Add(new InferredTypeProxy());
}
Type = new UserDefinedType(tok, cl.Name, cl, typeArgs);
+ UnresolvedType = Type;
}
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index a0dc2483..0b63a635 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1152,7 +1152,7 @@ namespace Microsoft.Dafny } else if (expr is LiteralExpr) {
var e = (LiteralExpr)expr;
if (e is StaticReceiverExpr) {
- return new StaticReceiverExpr(e.tok, e.Type);
+ return new StaticReceiverExpr(e.tok, CloneType(e.Type));
} else if (e.Value == null) {
return new LiteralExpr(e.tok);
} else if (e.Value is bool) {
@@ -3625,7 +3625,7 @@ namespace Microsoft.Dafny }
UserDefinedType aa = (UserDefinedType)a;
UserDefinedType bb = (UserDefinedType)b;
- if (aa.ResolvedClass != null && aa.ResolvedClass.Name == bb.ResolvedClass.Name) {
+ if (aa.ResolvedClass != null && aa.ResolvedClass == bb.ResolvedClass) {
// these are both resolved class/datatype types
Contract.Assert(aa.TypeArgs.Count == bb.TypeArgs.Count);
bool successSoFar = true;
@@ -5501,16 +5501,22 @@ namespace Microsoft.Dafny } else if (expr is LiteralExpr) {
LiteralExpr e = (LiteralExpr)expr;
- if (e.Value == null) {
- e.Type = new ObjectTypeProxy();
- } else if (e.Value is BigInteger) {
- e.Type = Type.Int;
- } else if (e.Value is bool) {
- e.Type = Type.Bool;
+
+ if (e is StaticReceiverExpr) {
+ StaticReceiverExpr eStatic = (StaticReceiverExpr)e;
+ this.ResolveType(eStatic.tok, eStatic.UnresolvedType, ResolveTypeOption.InferTypeProxies, null);
+ eStatic.Type = eStatic.UnresolvedType;
} else {
- Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal type
+ if (e.Value == null) {
+ e.Type = new ObjectTypeProxy();
+ } else if (e.Value is BigInteger) {
+ e.Type = Type.Int;
+ } else if (e.Value is bool) {
+ e.Type = Type.Bool;
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal type
+ }
}
-
} else if (expr is ThisExpr) {
if (!scope.AllowInstance) {
Error(expr, "'this' is not allowed in a 'static' context");
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 364e6c93..41cd8b02 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -2083,7 +2083,7 @@ Execution trace: (0,0): anon0
(0,0): anon11_Then
-Dafny program verifier finished with 46 verified, 8 errors
+Dafny program verifier finished with 49 verified, 8 errors
-------------------- Superposition.dfy --------------------
diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy index 684de262..0936176f 100644 --- a/Test/dafny0/AutoReq.dfy +++ b/Test/dafny0/AutoReq.dfy @@ -285,4 +285,15 @@ module StaticTest { {
g(y)
}
-}
\ No newline at end of file +
+ static predicate IsEven(x:int)
+
+ static function EvenDoubler(x:int) : int
+ requires IsEven(x);
+
+ // Should succeed thanks to auto-generated requirement of IsEven
+ static function {:autoReq} test(y:int) : int
+ {
+ EvenDoubler(y)
+ }
+}
|