summaryrefslogtreecommitdiff
path: root/Binaries
diff options
context:
space:
mode:
Diffstat (limited to 'Binaries')
-rw-r--r--Binaries/DafnyPrelude.bpl4
1 files changed, 0 insertions, 4 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index ad4dcbae..476a6bd9 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -207,7 +207,6 @@ axiom (forall b: BoxType :: { $Unbox(b): DatatypeType } $Box($Unbox(b): Datatype
type ClassName;
const unique class.int: ClassName;
const unique class.bool: ClassName;
-const unique class.object: ClassName;
const unique class.set: ClassName;
const unique class.seq: ClassName;
@@ -273,9 +272,6 @@ function DeclType<T>(Field T) returns (ClassName);
// -- Arrays -----------------------------------------------------
// ---------------------------------------------------------------
-function Array#Length(ref, int): int;
-axiom (forall r: ref, dim: int :: 0 <= Array#Length(r, dim));
-
procedure UpdateArrayRange(arr: ref, low: int, high: int, rhs: BoxType);
modifies $Heap;
ensures $HeapSucc(old($Heap), $Heap);