diff options
Diffstat (limited to 'BCT/BytecodeTranslator/Heap.cs')
| -rw-r--r-- | BCT/BytecodeTranslator/Heap.cs | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index 81f2b9e9..6bd552fa 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -51,6 +51,13 @@ procedure {:inline 1} Alloc() returns (x: int) $Alloc[x] := true;
}
+axiom (forall x : Field :: $DefaultStruct[x] == $DefaultBox);
+axiom Box2Int($DefaultBox) == 0;
+axiom Box2Bool($DefaultBox) == false;
+
+axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x );
+axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );
+
";
private Sink sink;
@@ -176,6 +183,13 @@ procedure {:inline 1} Alloc() returns (x: ref) $Alloc[x] := true;
}
+axiom (forall x : Field :: $DefaultStruct[x] == $DefaultBox);
+axiom Box2Int($DefaultBox) == 0;
+axiom Box2Bool($DefaultBox) == false;
+
+axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x );
+axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );
+
";
private Sink sink;
|