Module raw

Structs§

Code: A positive errno established by one native failure or completion field.
Count: One completed native count retaining its admitted ABI bound.
Descriptor: One live descriptor whose native producer or retained owner establishes its nonnegative domain, so later uses do not check that range again.
Exact: One native return whose producer reports exactly -1 or its one success value, so the ABI’s exactness proof is discharged once at admission and the decoder below is total without a second range check.
Status: A native scalar retained with the exact domain its producer guarantees, so every decoder below is total: the producer’s ABI proof is discharged once at construction and reused without a second range check.

Source: Access to errno immediately after a native operation reports failure.