int EVP_DigestFinal_ex()

in source/evp_override.c [827:845]

• 13 lines of code
• 4 McCabe index (conditional complexity)

int EVP_DigestFinal_ex(EVP_MD_CTX *ctx, unsigned char *md, unsigned int *s) {
    assert(ctx != NULL);
    assert(__CPROVER_w_ok(md, EVP_MD_CTX_size(ctx)));
    // s can be NULL

    *md = nondet_unsigned_char();

    if (s) *s = EVP_MD_CTX_size(ctx);
    ctx->digest = NULL; /* No additional calls to EVP_DigestUpdate. */

    if (nondet_bool()) {
        // Something went wrong, can't guarantee *s will have the correct value
        unsigned int garbage;
        if (s) *s = garbage;
        return 0;
    }

    return 1;
}