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 /Source/Dafny/DafnyAst.cs | |
| parent | 2dab50557b2584a82ffc7be8759d6a8a4720d1f9 (diff) | |
:autoReq now works with static functions.
This required fixing a small bug in how StaticReceiverExpr's were being handled
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 7 |
1 files changed, 7 insertions, 0 deletions
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
{
|