diff options
| author |  Unknown <qadeer@GHALIB.redmond.corp.microsoft.com> | 2011-05-17 16:57:37 -0700 |
|---|---|---|
| committer | Unknown <qadeer@GHALIB.redmond.corp.microsoft.com> | 2011-05-17 16:57:37 -0700 |
| commit | 23b62f2245437788238f93c63226d29f5526e12e (patch) | |
| tree | 64fb25c4d54bd802d6204b2ddd53872716127b42 | |
| parent | cc10a26c9a8d5cae6556a74958d2acfc8e4cb59d (diff) | |
added another axiom
| -rw-r--r-- | BCT/BytecodeTranslator/Heap.cs | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index 78774876..7ab72e82 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -60,6 +60,17 @@ procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref) {
$result := $TypeOf($DynamicType(this));
}
+axiom (forall t: Type :: $DynamicType($TypeOf(t)) == t);
+
+function $ThreadDelegate(Ref) : Ref;
+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
+{
+ assume $ThreadDelegate(this) == start$in;
+}
+procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
+{
+ call {:async} System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);
+}
";
private Sink sink;
@@ -203,6 +214,17 @@ procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref) {
$result := $TypeOf($DynamicType(this));
}
+axiom (forall t: Type :: $DynamicType($TypeOf(t)) == t);
+
+function $ThreadDelegate(Ref) : Ref;
+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
+{
+ assume $ThreadDelegate(this) == start$in;
+}
+procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
+{
+ call {:async} System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);
+}
";
private Sink sink;
|