diff options
| author |  Unknown <mbarnett@MIKE-SONY.redmond.corp.microsoft.com> | 2012-04-10 13:34:10 -0700 |
|---|---|---|
| committer | Unknown <mbarnett@MIKE-SONY.redmond.corp.microsoft.com> | 2012-04-10 13:34:10 -0700 |
| commit | 82820f7ed3d77561776cd87c84baca6e60028c26 (patch) | |
| tree | 66aabc2faad207a49525ac8227d7f3aeca9d2ae9 /BCT/BytecodeTranslator/Sink.cs | |
| parent | 5db02f7f6576b5d6814f8a5c4c7291f845ac557a (diff) | |
Added "free ensures" to procedures encoding the allocatedness
of references.
Diffstat (limited to 'BCT/BytecodeTranslator/Sink.cs')
| -rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index b1a8f1a4..8622c3a7 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -55,6 +55,7 @@ namespace BytecodeTranslator { }
}
}
+ this.uniqueNumberSeed = 0;
}
public Options Options { get { return this.options; } }
@@ -705,6 +706,35 @@ namespace BytecodeTranslator { }
}
#endregion
+
+ #region Add free ensures for allocatedness of result (for methods that return references)
+ if (retVariable != null && retVariable.TypedIdent.Type == this.Heap.RefType) {
+ var ens = new Bpl.Ensures(true,
+ Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Or,
+ Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,
+ Bpl.Expr.Ident(retVariable), Bpl.Expr.Ident(this.Heap.NullRef)),
+ Bpl.Expr.Select(Bpl.Expr.Ident(this.Heap.AllocVariable), Bpl.Expr.Ident(retVariable))
+ ));
+ boogiePostcondition.Add(ens);
+ }
+ #endregion
+ #region Add free ensures for preservation of allocatedness: AllocMapImplies(old($Alloc), $Alloc) == AllocMapConst(true)
+ var preserveAlloc = new Bpl.Ensures(true,
+ Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,
+ new Bpl.NAryExpr(
+ Bpl.Token.NoToken,
+ new Bpl.FunctionCall(this.Heap.AllocImplies),
+ new Bpl.ExprSeq(
+ new Bpl.OldExpr(Bpl.Token.NoToken, Bpl.Expr.Ident(this.Heap.AllocVariable)),
+ Bpl.Expr.Ident(this.Heap.AllocVariable))),
+ new Bpl.NAryExpr(
+ Bpl.Token.NoToken,
+ new Bpl.FunctionCall(this.Heap.AllocConstBool),
+ new Bpl.ExprSeq(Bpl.Expr.True))
+ ));
+ boogiePostcondition.Add(preserveAlloc);
+ #endregion
+
}
return procInfo;
}
@@ -1380,5 +1410,14 @@ namespace BytecodeTranslator { }
}
}
+
+ private int uniqueNumberSeed;
+ public int UniqueNumberAcrossAllAssemblies {
+ get {
+ return uniqueNumberSeed++;
+ }
+ }
+
+
}
}
\ No newline at end of file |