Skip to content
Topaz6.0 · Before release
Download

Search documentation

Specification 6.0 · Not released · Tested product 5.21.3

Use arrow keys to choose a result. Press Enter to open.

Type an API name, diagnostic number, rule, or project topic.

    Library · std.bytes

    ByteBuffer.get

    Reads the byte at an index in this buffer.

    get(index: int) -> int
    Module
    std.bytes
    Receiver
    ByteBuffer
    Minimum arity
    1
    Maximum arity
    1

    Declaration and parameters

    Link

    Availability

    Included by default: Pending

    Import std.bytes in language mode 5.21.

    The current compiler selects std/bytes.tpz for this language mode. Availability in other released editions and inclusion in each installed distribution are Pending.

    Source evidence

    Receiver

    ByteBuffer

    Parameter constraints

    Additional contracts are Pending.

    ByteBuffer.get and ByteBuffer.set use zero-based byte indices from zero through length minus one. Get returns an int byte.

    ByteBuffer.set replaces one byte. ByteBuffer.fill replaces length bytes beginning at start. Both require values from 0 through 255.

    ByteBuffer.copy receives the source buffer, sourceStart, targetStart, and length in that order. The receiver is the destination.

    Fill and copy use byte intervals from each start to start plus length. Starts and lengths must be nonnegative. Every complete source and destination interval must fit its buffer without arithmetic overflow.

    A zero length region at the end of a buffer is valid. A start beyond the end is invalid even when length is zero.

    Copy observes the source interval before its first destination write. Copying within one buffer therefore supports overlap in either direction.

    Set, fill, and copy return unit. They require a let mut root binding and update its destination value under collection value semantics.

    The receiver and supplied arguments evaluate once from left to right. Every range and byte check finishes before the first write.

    An invalid index or region produces TPZ4001 at runtime. An invalid byte value produces TPZ5001 at runtime, including a fill of zero bytes.

    A rejected operation performs no buffer writes. Effects performed while evaluating its receiver or arguments remain visible.

    When several preconditions fail, the selected failing precondition is unspecified. The operation still completes every argument evaluation before validation and performs no writes.

    Related rule: Validate buffer regions before writing

    Result

    Additional contracts are Pending.

    The declared result type is int.

    Effects

    Pending

    Failures

    Pending

    Result and effects

    Link

    Return the int byte at an in-range zero-based index. An invalid index produces TPZ4001 at runtime.

    Resolved contracts

    Link

    Related entries

    Link

    std.bytes

    Validate buffer regions before writing

    Link
    Ruletopaz.stdlib.contract.byte-buffer-mutation.rule

    Validate buffer regions before writing

    ByteBuffer.get and ByteBuffer.set use zero-based byte indices from zero through length minus one. Get returns an int byte.

    ByteBuffer.set replaces one byte. ByteBuffer.fill replaces length bytes beginning at start. Both require values from 0 through 255.

    ByteBuffer.copy receives the source buffer, sourceStart, targetStart, and length in that order. The receiver is the destination.

    Fill and copy use byte intervals from each start to start plus length. Starts and lengths must be nonnegative. Every complete source and destination interval must fit its buffer without arithmetic overflow.

    A zero length region at the end of a buffer is valid. A start beyond the end is invalid even when length is zero.

    Copy observes the source interval before its first destination write. Copying within one buffer therefore supports overlap in either direction.

    Set, fill, and copy return unit. They require a let mut root binding and update its destination value under collection value semantics.

    The receiver and supplied arguments evaluate once from left to right. Every range and byte check finishes before the first write.

    An invalid index or region produces TPZ4001 at runtime. An invalid byte value produces TPZ5001 at runtime, including a fill of zero bytes.

    A rejected operation performs no buffer writes. Effects performed while evaluating its receiver or arguments remain visible.

    When several preconditions fail, the selected failing precondition is unspecified. The operation still completes every argument evaluation before validation and performs no writes.

    Why

    Checking complete regions prevents a malformed count from leaving half-written data. Reading the source interval before writing gives one result for every overlap direction.

    Examples Copy overlapping regions and preserve an earlier buffer valueKeep an independent source buffer unchangedReject a read at the exclusive endReject a negative write indexReject a fill whose complete region does not fitReject an empty copy beyond the buffer endReject an invalid byte at a valid write indexValidate the byte for a fill of zero bytes

    Diagnostics TPZ4001TPZ5001

    Source evidence

    Copy overlapping regions and preserve an earlier buffer value

    Link

    run · running · Verification: not-run

    main.tpzCopy overlapping regions and preserve an earlier buffer valueOpen in Playground
    1. import std.bytes { Bytes, ByteBuffer }
    2. import std.io
    3. import std.test
    5. let mut buffer = ByteBuffer.fromBytes(test.assertOk(Bytes.fromHex("000102030405")))
    6. let alias = buffer
    7. buffer.copy(buffer, 0, 1, 5)
    8. io.writeLine(buffer.toBytes().toHex())
    9. buffer.fill(2, 2, 255)
    10. buffer.set(0, 128)
    11. io.writeLine(buffer.toBytes().toHex())
    12. buffer.copy(buffer, 1, 0, 5)
    13. buffer.fill(6, 0, 0)
    14. buffer.copy(buffer, 6, 6, 0)
    15. io.writeLine(buffer.toBytes().toHex())
    16. io.writeLine(alias.toBytes().toHex())
    17. io.writeLine("{alias.get(0)}")
    Expected outputexit 0
    000001020304
8000ffff0304
00ffff030404
000102030405
0
    $ topaz run main.tpz · target product 5.21.3
    Expected result

    Expected result

    Execution completes. Exit code 0.

    No stderr.

    Expected stdout
    1. 000001020304
    2. 8000ffff0304
    3. 00ffff030404
    4. 000102030405
    5. 0

    This exact example has not been executed.

    Source evidence

    Keep an independent source buffer unchanged

    Link

    run · running · Verification: not-run

    main.tpzKeep an independent source buffer unchangedOpen in Playground
    1. import std.bytes { ByteBuffer }
    2. import std.io
    4. let source = ByteBuffer.fromBytes("abc".encodeUtf8())
    5. let mut target = ByteBuffer.allocate(4, 0)
    6. target.copy(source, 1, 1, 2)
    7. io.writeLine(target.toBytes().toHex())
    8. io.writeLine(source.toBytes().toHex())
    Expected outputexit 0
    00626300
616263
    $ topaz run main.tpz · target product 5.21.3
    Expected result

    Expected result

    Execution completes. Exit code 0.

    No stderr.

    Expected stdout
    1. 00626300
    2. 616263

    This exact example has not been executed.

    Source evidence

    Reject a read at the exclusive end

    Link

    run · running · Verification: not-run

    main.tpzReject a read at the exclusive endOpen in Playground
    1. import std.bytes { ByteBuffer }
    2. let buffer = ByteBuffer.allocate(2)
    3. buffer.get(2)
    Expected outputNonzero exit
    No stdout.
    $ topaz run main.tpz · target product 5.21.3
    Expected result

    Expected result

    Rejection during run. Nonzero exit.

    • TPZ4001 byte-buffer-index-bounds at main.tpz:3:1

    No stdout.

    This exact example has not been executed.

    Source evidence

    Reject a negative write index

    Link

    run · running · Verification: not-run

    main.tpzReject a negative write indexOpen in Playground
    1. import std.bytes { ByteBuffer }
    2. let mut buffer = ByteBuffer.allocate(2)
    3. buffer.set(-1, 0)
    Expected outputNonzero exit
    No stdout.
    $ topaz run main.tpz · target product 5.21.3
    Expected result

    Expected result

    Rejection during run. Nonzero exit.

    • TPZ4001 byte-buffer-negative-bound at main.tpz:3:1

    No stdout.

    This exact example has not been executed.

    Source evidence

    Reject a fill whose complete region does not fit

    Link

    run · running · Verification: not-run

    main.tpzReject a fill whose complete region does not fitOpen in Playground
    1. import std.bytes { ByteBuffer }
    2. let mut buffer = ByteBuffer.allocate(2)
    3. buffer.fill(1, 2, 0)
    Expected outputNonzero exit
    No stdout.
    $ topaz run main.tpz · target product 5.21.3
    Expected result

    Expected result

    Rejection during run. Nonzero exit.

    • TPZ4001 byte-buffer-region-bounds at main.tpz:3:1

    No stdout.

    This exact example has not been executed.

    Source evidence

    Reject an empty copy beyond the buffer end

    Link

    run · running · Verification: not-run

    main.tpzReject an empty copy beyond the buffer endOpen in Playground
    1. import std.bytes { ByteBuffer }
    2. let mut buffer = ByteBuffer.allocate(2)
    3. buffer.copy(buffer, 3, 2, 0)
    Expected outputNonzero exit
    No stdout.
    $ topaz run main.tpz · target product 5.21.3
    Expected result

    Expected result

    Rejection during run. Nonzero exit.

    • TPZ4001 byte-buffer-region-bounds at main.tpz:3:1

    No stdout.

    This exact example has not been executed.

    Source evidence

    Reject an invalid byte at a valid write index

    Link

    run · running · Verification: not-run

    main.tpzReject an invalid byte at a valid write indexOpen in Playground
    1. import std.bytes { ByteBuffer }
    2. import std.io
    3. let mut buffer = ByteBuffer.allocate(1)
    4. buffer.set(0, -1)
    5. io.writeLine("after")
    Expected outputNonzero exit
    No stdout.
    $ topaz run main.tpz · target product 5.21.3
    Expected result

    Expected result

    Rejection during run. Nonzero exit.

    • TPZ5001 byte-buffer-byte-value at main.tpz:4:1

    No stdout.

    This exact example has not been executed.

    Source evidence

    Validate the byte for a fill of zero bytes

    Link

    run · running · Verification: not-run

    main.tpzValidate the byte for a fill of zero bytesOpen in Playground
    1. import std.bytes { ByteBuffer }
    2. import std.io
    3. let mut buffer = ByteBuffer.allocate(1)
    4. buffer.fill(1, 0, 256)
    5. io.writeLine("after")
    Expected outputNonzero exit
    No stdout.
    $ topaz run main.tpz · target product 5.21.3
    Expected result

    Expected result

    Rejection during run. Nonzero exit.

    • TPZ5001 byte-buffer-byte-value at main.tpz:4:1

    No stdout.

    This exact example has not been executed.

    Source evidence

    Diagnostics

    Link

    Index out of bounds

    Runtime value guard

    Menu

    Download