Tobias Reiher

The maintenance of some unit tests for the code generator is cumbersome due to their complexity. We should replace them by integration tests.

Enable getting the number of elements of a sequence. In the specification, this could be realized by using a Length attribute on a sequence variable: `Seq'Length`. Related to #51.

### Research #### Concepts - [Three-Address Code (TAC)](https://en.wikipedia.org/wiki/Three-address_code) - [Static single assignment form (SSA)](https://en.wikipedia.org/wiki/Static_single-assignment_form) - [Continuation-Passing Style (CPS)](https://en.wikipedia.org/wiki/Continuation-passing_style) #### Languages - [C Intermediate Language](https://github.com/cil-project/cil) ### Design #### Approach ``` Specification...

### Design idea - Store for each field one or multiple tuples of path condition and statically determined field location

### Objectives - Improve provability - Enable #107 Depends on #1228

Componolit/RecordFlux#736

### Basis https://github.com/Componolit/RecordFlux/tree/de4fcc7e114d06b8b8aaec78ee30082204d36ce6/tests/integration/session ### Standard - [RFC 8446](https://datatracker.ietf.org/doc/rfc8446/) - [Editorial update of RFC 8446](https://datatracker.ietf.org/doc/draft-ietf-tls-rfc8446bis/)

The calculation of the TCP checksum requires access to fields of the IP packet: > The checksum also covers a 96 bit pseudo header conceptually prefixed to the TCP header....

DTLS 1.3

1

The RFC is not finalized yet, but as far as I can tell, it should be very close. https://datatracker.ietf.org/doc/html/draft-ietf-tls-dtls13-41

Full test coverage of message specifications

3

The test coverage for all message specifications should be 100 %. Missing test data for a message should lead to an error instead of a warning.