Баг это ещё тот
Но, так сказать, для порядку:PROCEDURE (r: Reader) ReadBytes (VAR x: ARRAY OF BYTE; beg, len: INTEGER)
Код:
Pre
beg >= 0 20
len >= 0 21
beg + len <= LEN(x) 22
Post
r.Pos()' <= r.Base().Length() - len
r.Pos() = r.Pos()' + len
~r.eof
len bytes read after r.Pos()' and transferred into x
r.Pos()' > r.Base().Length() - len
r.Pos() = r.Base().Length()
r.eof
r.Base().Length() - r.Pos()' bytes read after r.Pos()' and transferred into x
Вариант len = 0 проходит по "первой" ветке. Всегда должен давать ~r.eof.beg >= 0 20
len >= 0 21
beg + len <= LEN(x) 22
Post
r.Pos()' <= r.Base().Length() - len
r.Pos() = r.Pos()' + len
~r.eof
len bytes read after r.Pos()' and transferred into x
r.Pos()' > r.Base().Length() - len
r.Pos() = r.Base().Length()
r.eof
r.Base().Length() - r.Pos()' bytes read after r.Pos()' and transferred into x
Реализация в HostFiles при len = 0 не изменяет r.eof.
Код:
PROCEDURE (r: Reader) ReadBytes (VAR x: ARRAY OF BYTE; beg, len: INTEGER);
VAR from, to, count, restInBuf: INTEGER;
BEGIN (* portable *)
ASSERT(beg >= 0, 21);
IF len > 0 THEN
...
ELSE ASSERT(len = 0, 22)
END
END ReadBytes;
VAR from, to, count, restInBuf: INTEGER;
BEGIN (* portable *)
ASSERT(beg >= 0, 21);
IF len > 0 THEN
...
ELSE ASSERT(len = 0, 22)
END
END ReadBytes;