int i2d_ASN1_INTEGER()

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;
}