diff options
| author |  Unknown <qadeer@GHALIB.redmond.corp.microsoft.com> | 2011-05-18 23:25:29 -0700 |
|---|---|---|
| committer | Unknown <qadeer@GHALIB.redmond.corp.microsoft.com> | 2011-05-18 23:25:29 -0700 |
| commit | a48f2cc95e01742e8d1a6c3e69846598ee2a91a2 (patch) | |
| tree | 92b2652ad56f167feabda4c86f38f8b1e6af4aa6 /BCT | |
| parent | f90a2fd212c8e4893b37aa9bfa5e6ed70d882702 (diff) | |
fixed the axiom about TypeOf
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)
|