Tobias Reiher
Tobias Reiher
The length of an sequence is often defined by a length field. But some protocols like USB and DNS only specify the number of elements of an sequence. In such...
It should be possible to define invariants for sequences, e.g. show that a sequence contains no duplicates: ```Ada type Extensions is sequence of Extension with Invariant => (for all I...
Examples are the options fields of IPv4 and CoAP. The end marker is only present in IPv4, if the end of the last option does not match the end of...
References or pointers can be used to refer to other parts of the message. The [message compression mechanism of DNS](https://tools.ietf.org/html/rfc1035#section-4.1.4) is using pointers to prevent the repetition of domain names....
One TLS 1.3 message needs to be parsed from right to left. An optional and variable number of zero bytes must be read until a marker (`Content_Type`) is found. All...
`GNAT.Sockets` cannot be directly used with the generated SPARK code, as the buffer type `Ada.Streams.Stream_Element_Array` is incompatible. ```Ada type Stream_Element is mod 2 ** Standard'Storage_Unit; type Stream_Element_Offset is new Long_Long_Integer;...
We are unable to detect potential failing range checks in the model. Here is an example: ```Ada package Test is type A is mod 2 ** 32; type B is...
Required for NTP.
> The three byte offset to next extension indicates the position of the > next extension as offset from the beginning of the SLP message. > > The offset value...
From time to time, the scheduled CI tests fail because of exceeding the maximum execution time. In the most cases, it's caused by the `Tests (python_coverage, 3.7)` job. Example: https://github.com/Componolit/RecordFlux/actions/runs/2854204042