Update aws_byte_buf_is_bounded to include a null check
adpaco-aws opened this issue · 1 comments
adpaco-aws commented
This would avoid having the following code in proofs:
__CPROVER_assume(buf1 != NULL);
__CPROVER_assume(aws_byte_buf_is_bounded(buf1, MAX_BUFFER_SIZE));
ensure_byte_buf_has_allocated_buffer_member(buf1);
__CPROVER_assume(aws_byte_buf_is_valid(buf1));
by removing the first line (which should be done in aws_byte_buf_is_bounded
in any case)
feliperodri commented
@adpaco-aws This issue should be moved to AWS C Common. Then we just need to update the version of the submodule here.