diff options
| author |  Unknown <t-espave@A3479886.redmond.corp.microsoft.com> | 2011-07-15 16:38:27 -0700 |
|---|---|---|
| committer | Unknown <t-espave@A3479886.redmond.corp.microsoft.com> | 2011-07-15 16:38:27 -0700 |
| commit | 759c72c8a72be819b16e249578bae9fdb68c45a7 (patch) | |
| tree | 66e81049a696adc648ecd85e564b66cdff086b40 /BCT | |
| parent | 345a34991828aa94f7067e30720aba9d0f416960 (diff) | |
potentially useful boogie stubs, commented out since they may conflict with {:extern}
Diffstat (limited to 'BCT')
| -rw-r--r-- | BCT/BytecodeTranslator/HeapFactory.cs | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs index fa46fe34..09318f65 100644 --- a/BCT/BytecodeTranslator/HeapFactory.cs +++ b/BCT/BytecodeTranslator/HeapFactory.cs @@ -451,6 +451,48 @@ procedure DelegateRemoveHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref) }
}
+//procedure System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);
+//procedure System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);
+//
+//implementation System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool) {
+// $result := (a$in == b$in);
+//}
+//
+//implementation System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool) {
+// $result := (a$in != b$in);
+//}
+//
+//// SILVERLIGHT CONTROL SPECIFIC CODE
+//function isControlEnabled(Ref) : bool;
+//function isControlChecked(Ref) : bool;
+//
+//procedure System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool);
+//implementation System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool) {
+// assume isControlEnabled($this) == value$in;
+//}
+//
+//procedure System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref);
+//implementation System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref) {
+// var enabledness: bool;
+// enabledness := isControlEnabled($this);
+// $result := Box2Ref(Bool2Box(enabledness));
+//}
+//
+//procedure System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref);
+//implementation System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref) {
+// var check: bool;
+//
+// check := Box2Bool(Ref2Box(value$in));
+// assume isControlChecked($this) == check;
+//}
+//
+//procedure System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref);
+//implementation System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref) {
+// var isChecked: bool;
+// isChecked := isControlChecked($this);
+// $result := Box2Ref(Bool2Box(isChecked));
+//}
+
";
[RepresentationFor("$Head", "var $Head: [Ref]Ref;")]
|