int EVP_PKEY_derive()

in source/evp_override.c [227:251]

• 20 lines of code
• 3 McCabe index (conditional complexity)

int EVP_PKEY_derive(EVP_PKEY_CTX *ctx, unsigned char *key, size_t *keylen) {
    /* TODO: assert(evp_pkey_ctx_is_valid(ctx)); */
    assert(ctx != NULL);
    assert(ctx->is_initialized_for_derivation == true);
    assert(keylen);
    // Derivation size is nondeterministic but fixed. See ec_override.c for details.
    size_t max_required_size = max_derivation_size();

    if (nondet_bool()) {
        int rv;
        __CPROVER_assume(rv <= 0);
        return rv;
    }

    if (!key) {
        *keylen = max_required_size;
    } else {
        size_t amount_of_data_written;
        __CPROVER_assume(amount_of_data_written <= *keylen);
        write_unconstrained_data(key, amount_of_data_written);
        *keylen = amount_of_data_written;
    }

    return 1;
}