Prevent unnecessary checks in session states

[treiher]

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 disabled (#670). There is currently not enough information in the code generator to decide whether a property is already established or requires verification.

Use Cases

Removing the unnecessary code will improve the efficiency and binary size of the generated code (#908).

Considered Options

O1 Consider contracts of statements and states

• The pre- and post-conditions are determined for each statement.
• The necessity of a check is inferred based on the pre-conditions of the statement and the current facts.
• The facts are established by the post-conditions of all previous statements and the pre-conditions of the state.
• The post-condition of a state is equivalent to the established facts after the last statement of the state.
• The pre-condition of a state is a disjunction, where each disjunct is a conjunction of the post-condition and transition condition of all possible predecessor states (exception transitions will not be considered).

Decision Outcome

O1

[treiher]

There are several checks, where SPARK is able to show that these checks are unnecessary. The code generator does not yet contain the necessary information to come to the same conclusion. This will probably change with the work for #691.