Client side: assertion fails in session_request_handles_bs in degraded cases
Description
In degraded cases the assertion session_request_handles_bs.c:line 58
might fail
assert(client_requests[session_request_handle_bs__req_handle] == constants__c_session_indet);
Analysis
It occurs when a session was recorded for a given request handle (when generating a request) and the response is never received or an invalid response is received with the same request handle. Then if the same request handle is used later on a session the assertion will fail since request handle was considered as used.
Fixes
Since the freshness of the request handle is managed by request_handle_bs
module, it is not necessary to do this assertion here and it is valid to overwrite old data in this case. It is guaranteed by B model using request_handle_bs
that it is legit and we do not need to maintain validity of request handle in session_request_handles_bs
.
- Remove assertion
- Add unit test of
request_handles_bs
C module to guarantee C implementation is not faulty
Edited by Vincent Monfort