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

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.

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