Bug in text_file_read.e

[Guillaume Lemaître-2]

  Hi,

I think there is a mistake in filtered_unread_character. To me it should look like this :

filtered_unread_character is

do

end_of_input := False

buffer_position := buffer_position - 1

filtered_last_character := buffer.item(buffer_position - 1)

end

What do you think ?

Guillaume

[Cyril ADRIAN]

Hi Guillaume,

On Sun, Apr 6, 2008 at 9:08 PM, Guillaume Lemaître
<guillaume.lemaitre@...> wrote:
>  I think there is a mistake in filtered_unread_character. To me it should
>  look like this :
>
>  What do you think ?

After having read the source I think you are right. I committed your fix.

Best regards,
--
Cyril ADRIAN - http://www.cadrian.net/~cyril

Any problem can be solved by another layer of indirection.
But that usually will create another problem.
-- David Wheeler

[Guillaume Lemaître-2]

Nevertheless, I think there are more problematic issues as one can unread as many characters as he wants to :
  - no precaution is taken not to unread more characters than were read
  - read/unread at the beginning of the file is possible, but now crashes as we try to read before the head of the buffer
  - read/unread at the limit of the buffer should not work neither

I will try to provide later fixes for those issues.

2008/4/7, Cyril ADRIAN <cyril.adrian@...>:

Hi Guillaume,


On Sun, Apr 6, 2008 at 9:08 PM, Guillaume Lemaître
<guillaume.lemaitre@...> wrote:
>  I think there is a mistake in filtered_unread_character. To me it should
>  look like this :
>

>  What do you think ?

After having read the source I think you are right. I committed your fix.

Best regards,

--
Cyril ADRIAN - http://www.cadrian.net/~cyril

Any problem can be solved by another layer of indirection.
But that usually will create another problem.
-- David Wheeler

[Guillaume Lemaître-2]

  Hello Cyril

In fact your last fix now breaks the post condition of read_character, I mean 'not end_of_input implies can_unread_character', as we cannot unread the first character read from the buffer.

2008/4/8, Cyril ADRIAN <cyril.adrian@...>:

On Mon, Apr 7, 2008 at 9:05 PM, Guillaume Lemaître

<guillaume.lemaitre@...> wrote:

> Nevertheless, I think there are more problematic issues as one can unread as
>  many characters as he wants to :
>   - no precaution is taken not to unread more characters than were read
>   - read/unread at the beginning of the file is possible, but now crashes as
>  we try to read before the head of the buffer
>   - read/unread at the limit of the buffer should not work neither


OK, it looks like the precondition (can_unread_buffer) is broken.

In fact, buffer_position is not the index of the last character, but
the index of the next character.

(fix committed)


Best regards,
--
Cyril ADRIAN - http://www.cadrian.net/~cyril

Any problem can be solved by another layer of indirection.
But that usually will create another problem.
-- David Wheeler

[Raphael Mack-2]

Hi,

sorry, that I have to revive this thread. But it seems to be actually still
in. I don't know the concept of unreading characters and all that stuff. I
just see, that e. g. the XML parser is broken by the cyrils commit r8945
of TEXT_FILE_READ. Would be cool, if anyone could help...

Rapha

Am Freitag, 11. April 2008 schrieb Guillaume Lemaître:

>   Hello Cyril
>
> In fact your last fix now breaks the post condition of read_character, I
> mean 'not end_of_input implies can_unread_character', as we cannot
> unread the first character read from the buffer.
>
> 2008/4/8, Cyril ADRIAN <cyril.adrian@...>:
> > On Mon, Apr 7, 2008 at 9:05 PM, Guillaume Lemaître
> >
> > <guillaume.lemaitre@...> wrote:
> > > Nevertheless, I think there are more problematic issues as one can
> >
> > unread as
> >
> > >  many characters as he wants to :
> > >   - no precaution is taken not to unread more characters than were
> > > read - read/unread at the beginning of the file is possible, but now
> >
> > crashes as
> >
> > >  we try to read before the head of the buffer
> > >   - read/unread at the limit of the buffer should not work neither
> >
> > OK, it looks like the precondition (can_unread_buffer) is broken.
> >
> > In fact, buffer_position is not the index of the last character, but
> > the index of the next character.
> >
> > (fix committed)
> >
> >
> > Best regards,
> > --
> > Cyril ADRIAN - http://www.cadrian.net/~cyril
> >
> > Any problem can be solved by another layer of indirection.
> > But that usually will create another problem.
> > -- David Wheeler