Tobias Reiher
Tobias Reiher
### Context and Problem Statement Some error handling in the generated session code is unnecessary and could be removed. We currently do not detect such issues because proof warnings are...
After the refactoring in #659 several unreachable branches are detected by GNATprove, which were not found before. All affected branches should be replaced by `raise Program_Error` to suppress the warnings....
The following session specification must not be accepted, as the final state is not a null state. A final state is never executed, so it doesn't make sense to define...
`SessionGenerator._ensure` is difficult to understand. Since the removal of deferred exceptions, it could probably be replaced by the much simpler `SessionGenerator._raise_exception_if`.
`Field_Condition` has to be checked when setting field values in cases where conditions could be violated. Part of #691.
### Context and Problem Statement Currently, it is possible to access fields of an incomplete or even partially invalid message, as only the validity of a single field is checked...
Basis: [Hypothesis](https://github.com/HypothesisWorks/hypothesis) ### Property-Based Test for Model Parser - Generate model - Convert to specification - Parse specification - Compare models To be tested entities: - [x] ModularInteger - [x]...
### Context and Problem Statement In some cases, the style checks cannot be fulfilled or it is not intended to fulfill all style checks. In such cases, it should be...
As `Model` stores types and session in two separate lists, the order of type declarations and session declarations is lost when parsing a specification. Consequently, the specification generated from a...
### Context and Problem Statement In some cases, it would be beneficial to parameterize the code generation. ### Use Cases - UC1 Enable different feature sets (i.e. remove parts of...