aws/aws-encryption-sdk-c

Update aws_byte_buf_is_bounded to include a null check

Opened this issue · 1 comments

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)

@adpaco-aws This issue should be moved to AWS C Common. Then we just need to update the version of the submodule here.