diff options
| author |  Mike Barnett <mbarnett@microsoft.com> | 2011-05-19 13:26:13 -0700 |
|---|---|---|
| committer | Mike Barnett <mbarnett@microsoft.com> | 2011-05-19 13:26:13 -0700 |
| commit | 03b24df6c2fa4217f74d3cc76785ab6babbe6f2f (patch) | |
| tree | 02004c12ab9b045e00c5f552e5d66a5c76c54e83 /BCT | |
| parent | 0a1cb72eec7026923f21a097e80d161f9c86fb44 (diff) | |
| parent | 9087bb0fbc57c065ce9f0c3d1b1dbf4a67bd4a3d (diff) | |
Merge
Diffstat (limited to 'BCT')
| -rw-r--r-- | BCT/BytecodeTranslator/Heap.cs | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index 28964c15..87d950c4 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -60,7 +60,8 @@ procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref) {
$result := $TypeOf($DynamicType(this));
}
-axiom (forall t: Type :: $DynamicType($TypeOf(t)) == t);
+function $TypeOfInv(Ref): Type;
+axiom (forall t: Type :: {$TypeOf(t)} $TypeOfInv($TypeOf(t)) == t);
function $ThreadDelegate(Ref) : Ref;
@@ -226,7 +227,8 @@ procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref) {
$result := $TypeOf($DynamicType(this));
}
-axiom (forall t: Type :: $DynamicType($TypeOf(t)) == t);
+function $TypeOfInv(Ref): Type;
+axiom (forall t: Type :: {$TypeOf(t)} $TypeOfInv($TypeOf(t)) == t);
function $ThreadDelegate(Ref) : Ref;
procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
|