From e0f4d19e19d3cd09acaaec91bef529fc49d0c378 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 11 Feb 2013 18:49:28 -0800 Subject: Reverted some accidental changes to a test case --- Test/vstte2012/RingBufferAuto.dfy | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) (limited to 'Test/vstte2012') diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy index 73a6c3fd..f51a36b2 100644 --- a/Test/vstte2012/RingBufferAuto.dfy +++ b/Test/vstte2012/RingBufferAuto.dfy @@ -43,18 +43,9 @@ class {:autocontracts} RingBuffer } method Enqueue(x: T) - //requires |Contents| != N; - ensures Contents == old(Contents) + [x] && N >= old(N); + requires |Contents| != N; + ensures Contents == old(Contents) + [x] && N == old(N); { - if (len == data.Length) { - var more := data.Length; - var d := new T[data.Length + more]; - parallel (i | 0 <= i < data.Length) { - d[if i < start then i else i + more] := data[i]; - } - data := d; - N, start := N + more, start + more; - } var nextEmpty := if start + len < data.Length then start + len else start + len - data.Length; data[nextEmpty] := x; -- cgit v1.2.3