diff options
Diffstat (limited to 'Dafny')
| -rw-r--r-- | Dafny/DafnyAst.cs | 11 | ||||
| -rw-r--r-- | Dafny/Resolver.cs | 2 | ||||
| -rw-r--r-- | Dafny/Translator.cs | 7 |
3 files changed, 19 insertions, 1 deletions
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index 04b6b00e..e07c6f1d 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -867,6 +867,17 @@ namespace Microsoft.Dafny { }
}
+ public class DatatypeDestructor : SpecialField
+ {
+ public readonly DatatypeCtor EnclosingCtor;
+
+ public DatatypeDestructor(IToken tok, DatatypeCtor enclosingCtor, string name, string compiledName, string preString, string postString, bool isGhost, Type type, Attributes attributes)
+ : base(tok, name, compiledName, preString, postString, isGhost, false, type, attributes)
+ {
+ EnclosingCtor = enclosingCtor;
+ }
+ }
+
public class CouplingInvariant : MemberDecl {
public readonly Expression Expr;
public readonly List<IToken/*!*/>/*!*/ Toks;
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index df2d2b0b..b6bc4059 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -254,7 +254,7 @@ namespace Microsoft.Dafny { if (members.ContainsKey(formal.Name)) {
Error(ctor, "Name of deconstructor is used by another member of the datatype: {0}", formal.Name);
} else {
- dtor = new SpecialField(formal.tok, formal.Name, "dtor_" + formal.Name, "", "", false, false, formal.Type, null);
+ dtor = new DatatypeDestructor(formal.tok, ctor, formal.Name, "dtor_" + formal.Name, "", "", formal.IsGhost, formal.Type, null);
dtor.EnclosingClass = dt; // resolve here
members.Add(formal.Name, dtor);
}
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index 37f80bf1..028891b5 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -1650,6 +1650,9 @@ namespace Microsoft.Dafny { var t = IsTotal(e.Obj, etran);
if (e.Obj.Type.IsRefType) {
t = BplAnd(t, Bpl.Expr.Neq(etran.TrExpr(e.Obj), predef.Null));
+ } else if (e.Field is DatatypeDestructor) {
+ var dtor = (DatatypeDestructor)e.Field;
+ t = BplAnd(t, FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullName, Bpl.Type.Bool, etran.TrExpr(e.Obj)));
}
return t;
}
@@ -2110,6 +2113,10 @@ namespace Microsoft.Dafny { CheckWellformed(e.Obj, options, locals, builder, etran);
if (e.Obj.Type.IsRefType) {
CheckNonNull(expr.tok, e.Obj, builder, etran, options.AssertKv);
+ } else if (e.Field is DatatypeDestructor) {
+ var dtor = (DatatypeDestructor)e.Field;
+ builder.Add(Assert(expr.tok, FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullName, Bpl.Type.Bool, etran.TrExpr(e.Obj)),
+ string.Format("destructor '{0}' can only be applied to datatype values constructed by '{1}'", dtor.Name, dtor.EnclosingCtor.Name)));
}
if (options.DoReadsChecks && e.Field.IsMutable) {
builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), etran.TrExpr(e.Obj), GetField(e)), "insufficient reads clause to read field", options.AssertKv));
|