Improve B model for session handling
B model for session handling should provide more guarantees to C code:
- Validity of some session parameters is not always guaranteed and should be to avoid defensive C code (e.g.: application context in
session_core_bs__notify_set_session_state
) - Operations of
session_core
should ensure session validity internally (session : s_session
) if exposed bysession_mgr
which does not exposes_session
- Session validity verification in
session_mgr_i
operations that usesession_core
operations with validity precondition is often not straightforward. - Client / Server session sets should be differentiated to allow providing more precise invariants