PR# 18559 check_buffer in SED_MEMORY_READER_WRITER is not correct for all values of n

Problem Report Summary
Submitter: finnianr
Category: EiffelBase
Priority: High
Date: 2013/03/27
Class: Bug
Severity: Critical
Number: 18559
Release: 7.2.9.1351
Confidential: No
Status: Closed
Responsible:
Environment: Windows 7, Ubuntu 12.10
Synopsis: check_buffer in SED_MEMORY_READER_WRITER is not correct for all values of n

Description
Consider the operation of check_buffer for the following values:

count is 0
buffer.count is 500
buffer_size is 500
n is 1500

If there was a post-condition to check if the buffer is big enough, would it pass? The answer of course is no.

feature {NONE} -- Buffer update

   check_buffer (n: INTEGER)
         -- If there is enough space in `buffer' to read `n' bytes, do nothing.
         -- Otherwise, read/write to `medium' to free some space.
      do
         if n + count > buffer_size then
            buffer.resize (buffer.count + buffer.count // 2)
            buffer_size := buffer.count
         end
      end

I have put the severity as critical because it is crashing my app.
To Reproduce

										
Problem Report Interactions
From:manus_eiffel    Date:2013/03/27    Status: Closed    Download   
Thanks for the report. This is now fixed in rev#92366.

the new code we have is:

	check_buffer (n: INTEGER)
			-- If there is enough space in `buffer' to read `n' bytes, do nothing.
		do
			if n + count > buffer_size then
				buffer.resize ((n + count).max (buffer.count + buffer.count // 2))
				buffer_size := buffer.count
			end
		ensure then
			buffer_adapted: n + count <= buffer_size
		end