Verification of session model

[treiher]

Motivation

• Enable creation of automatically provable SPARK code (e.g., prevent access to uninitialized variables, statically false conditions, length-mismatches in message instantiations)

Description

• Enhance type system (e.g., typestate analysis)
• Implement data-flow analysis

Tasks

• [ ] Detect always false preconditions
• [ ] https://github.com/Componolit/RecordFlux/issues/451
• [ ] https://github.com/Componolit/RecordFlux/issues/452
• [x] Ensure final state is null state
• [x] https://github.com/Componolit/RecordFlux/issues/977
• [ ] Detect unused variables and assigned but never read variables