Remove is_valid_* operations from message_*_bs
The basic machines message_in_bs
and message_out_bs
contain several query operations:
is_valid_msg_in_type
is_valid_msg_in_header
is_valid_msg_in
is_valid_buffer_out
is_valid_msg_out
is_valid_msg_out_header
that promise more than is implemented: in these operations, the computation of the output parameters depends on some abstract variables which are not implemented in the C code. Therefore, their implementation does not really refine their specification.
Moreover, these operations are always called with a parameter which is just computed by the same B machine. It would be simpler to add a second output parameter to the computing operation for returning the validity of the result and remove these operations.
Note: this issue is related to #1015 (closed).