diff options
| author |  Bryan Parno <parno@microsoft.com> | 2014-01-08 16:59:22 -0800 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2014-01-08 16:59:22 -0800 |
| commit | 709f460287dac7b6646fe770d3e01ed7cf26c9eb (patch) | |
| tree | 41a6b4fd1f59b411cb6b84be871a36969f73c6b0 | |
| parent | 2dab50557b2584a82ffc7be8759d6a8a4720d1f9 (diff) | |
:autoReq now works with static functions.
This required fixing a small bug in how StaticReceiverExpr's were being handled
| -rw-r--r-- | Source/Dafny/Cloner.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 7 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 4 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/AutoReq.dfy | 19 |
5 files changed, 33 insertions, 3 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 55b23827..ba30af5c 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -200,7 +200,9 @@ namespace Microsoft.Dafny return null;
} else if (expr is LiteralExpr) {
var e = (LiteralExpr)expr;
- if (e.Value == null) {
+ if (e is StaticReceiverExpr) {
+ return new StaticReceiverExpr(e.tok, e.Type);
+ } else if (e.Value == null) {
return new LiteralExpr(Tok(e.tok));
} else if (e.Value is bool) {
return new LiteralExpr(Tok(e.tok), (bool)e.Value);
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 6908a373..5525e879 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -4169,6 +4169,13 @@ namespace Microsoft.Dafny { /// </summary>
public class StaticReceiverExpr : LiteralExpr
{
+ public StaticReceiverExpr(IToken tok, Type t)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(t != null);
+ Type = t;
+ }
+
public StaticReceiverExpr(IToken tok, ClassDecl cl)
: base(tok) // constructs a LiteralExpr representing the 'null' literal
{
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 1fba4170..5063733c 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1151,7 +1151,9 @@ namespace Microsoft.Dafny return null;
} else if (expr is LiteralExpr) {
var e = (LiteralExpr)expr;
- if (e.Value == null) {
+ if (e is StaticReceiverExpr) {
+ return new StaticReceiverExpr(e.tok, e.Type);
+ } else if (e.Value == null) {
return new LiteralExpr(e.tok);
} else if (e.Value is bool) {
return new LiteralExpr(e.tok, (bool)e.Value);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index c46f780c..424fe0bd 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 43 verified, 8 errors
+Dafny program verifier finished with 46 verified, 8 errors
-------------------- Superposition.dfy --------------------
diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy index 00c74f50..684de262 100644 --- a/Test/dafny0/AutoReq.dfy +++ b/Test/dafny0/AutoReq.dfy @@ -266,4 +266,23 @@ module Matches { }
}
+// Make sure :autoReq works with static functions
+module StaticTest {
+ static function f(x:int) : bool
+ requires x > 3;
+ {
+ x > 7
+ }
+ static function {:autoReq} g(z:int) : bool
+ requires f(z);
+ {
+ true
+ }
+
+ // Should succeed thanks to auto-generation based on f's requirements
+ static function {:autoReq} h(y:int) : bool
+ {
+ g(y)
+ }
+}
\ No newline at end of file |