diff options
author | 2011-05-04 21:43:06 -0700 | |
---|---|---|
committer | 2011-05-04 21:43:06 -0700 | |
commit | 5b3377c63d15b6f5291cd76f88be9123970a4701 (patch) | |
tree | c7b1fd66797d8ca2b6edc534c42187d1b19871b4 | |
parent | 399a8aa59b472cfa800ae8a97b0d15aaa86b4d59 (diff) |
added a few more axioms
-rw-r--r-- | BCT/BytecodeTranslator/Heap.cs | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index 1776d26b..58a74d53 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -35,24 +35,26 @@ namespace BytecodeTranslator { private readonly string InitialPreludeText =
@"type Struct = [Field]Box;
type HeapType = [Ref,Field]Box;
-var $Heap: HeapType where IsGoodHeap($Heap);
-function IsGoodHeap(HeapType): bool;
+var $Heap: HeapType;
var $Alloc: [Ref] bool;
procedure {:inline 1} Alloc() returns (x: Ref)
- free ensures x != null;
modifies $Alloc;
{
- assume $Alloc[x] == false;
+ assume $Alloc[x] == false && x != null;
$Alloc[x] := true;
}
axiom (forall x : Field :: $DefaultStruct[x] == $DefaultBox);
axiom Box2Int($DefaultBox) == 0;
axiom Box2Bool($DefaultBox) == false;
+axiom Box2Ref($DefaultBox) == null;
+axiom Box2Struct($DefaultBox) == $DefaultStruct;
axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x );
axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );
+axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x );
+axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
";
private Sink sink;
@@ -154,7 +156,7 @@ axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x ); #region Fields
- [RepresentationFor("$Heap", "var $Heap: HeapType where IsGoodHeap($Heap);", true)]
+ [RepresentationFor("$Heap", "var $Heap: HeapType;", true)]
private Bpl.Variable HeapVariable = null;
[RepresentationFor("Read", "function {:inline true} Read(H:HeapType, o:Ref, f:Field): Box { H[o, f] }")]
@@ -169,23 +171,25 @@ axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x ); private readonly string InitialPreludeText =
@"type Struct = [Field]Box;
type HeapType = [Ref,Field]Box;
-function IsGoodHeap(HeapType): bool;
var $Alloc: [Ref] bool;
procedure {:inline 1} Alloc() returns (x: Ref)
- free ensures x != null;
modifies $Alloc;
{
- assume $Alloc[x] == false;
+ assume $Alloc[x] == false && x != null;
$Alloc[x] := true;
}
axiom (forall x : Field :: $DefaultStruct[x] == $DefaultBox);
axiom Box2Int($DefaultBox) == 0;
axiom Box2Bool($DefaultBox) == false;
+axiom Box2Ref($DefaultBox) == null;
+axiom Box2Struct($DefaultBox) == $DefaultStruct;
axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x );
axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );
+axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x );
+axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
";
private Sink sink;
|