in source/asn1_override.c [106:124]
int i2d_ASN1_INTEGER(ASN1_INTEGER *a, unsigned char **ppout) {
assert(asn1_integer_is_valid(a));
assert(ppout);
assert(!*ppout); // Assuming is always called with *ppout == NULL, therefore needs to allocated the buffer
int buf_size;
__CPROVER_assume(0 < buf_size);
*ppout = malloc(buf_size);
if (!*ppout) {
int error_code;
__CPROVER_assume(error_code < 0);
return error_code;
}
// Since the buffer is allocated internally, don't need to increment
return buf_size;
}