summaryrefslogtreecommitdiff
path: root/BCT/BytecodeTranslator/Heap.cs
diff options
context:
space:
mode:
Diffstat (limited to 'BCT/BytecodeTranslator/Heap.cs')
-rw-r--r--BCT/BytecodeTranslator/Heap.cs2
1 files changed, 2 insertions, 0 deletions
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 283a59a3..f38e0093 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -39,6 +39,7 @@ var $Heap: HeapType;
var $Alloc: [Ref] bool;
procedure {:inline 1} Alloc() returns (x: Ref)
+ free ensures x != null;
modifies $Alloc;
{
assume $Alloc[x] == false && x != null;
@@ -175,6 +176,7 @@ type HeapType = [Ref,Field]Box;
var $Alloc: [Ref] bool;
procedure {:inline 1} Alloc() returns (x: Ref)
+ free ensures x != null;
modifies $Alloc;
{
assume $Alloc[x] == false && x != null;