Skip to content

Commit 900998a

Browse files
committed
Address TODO in streams.py
1 parent 2ae8391 commit 900998a

File tree

1 file changed

+4
-2
lines changed
  • TestModels/dafny-dependencies/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern

1 file changed

+4
-2
lines changed

TestModels/dafny-dependencies/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/streams.py

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,10 @@ def __init__(self, dafny_byte_stream):
1717
self.dafny_byte_stream = dafny_byte_stream
1818

1919
def read(self, size: int = -1) -> bytes:
20-
# TODO: assert size is -1, buffer,
21-
# or define a more specialized Action<int, bytes> type for streams.
20+
# We could define a more specialized Action<int, bytes> type for streams
21+
# if we wanted to support this level of control in all languages.
22+
if size != -1:
23+
raise ValueError(f"A read size other than -1 is not supported: {size}")
2224
next = self.dafny_byte_stream.Next()
2325
while next.is_Some and len(next.value) == 0:
2426
next = self.dafny_byte_stream.Next()

0 commit comments

Comments
 (0)