From f5b9f70c1da3279581cd910ce56a3d840e151f14 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 26 Oct 2011 20:55:53 -0700 Subject: Dafny: removed support for assigning to an array-range (that is, an assignment statement where the LHS has the form a[lo..hi]) --- Binaries/DafnyPrelude.bpl | 7 ------- 1 file changed, 7 deletions(-) (limited to 'Binaries') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 32430fd3..1fe21204 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -489,13 +489,6 @@ axiom (forall r: ref, h: HeapType :: function array.Length(a: ref): int; axiom (forall o: ref :: 0 <= array.Length(o)); -procedure UpdateArrayRange(arr: ref, low: int, high: int, rhs: BoxType); - modifies $Heap; - ensures $HeapSucc(old($Heap), $Heap); - ensures (forall i: int :: { read($Heap, arr, IndexField(i)) } low <= i && i < high ==> read($Heap, arr, IndexField(i)) == rhs); - ensures (forall o: ref, f: Field alpha :: { read($Heap, o, f) } read($Heap, o, f) == read(old($Heap), o, f) || - (o == arr && FDim(f) == 1 && low <= IndexField_Inverse(f) && IndexField_Inverse(f) < high)); - // --------------------------------------------------------------- // -- The heap --------------------------------------------------- // --------------------------------------------------------------- -- cgit v1.2.3