int EVP_PKEY_encrypt()

in source/evp_override.c [337:358]

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

int EVP_PKEY_encrypt(EVP_PKEY_CTX *ctx, unsigned char *out, size_t *outlen, const unsigned char *in, size_t inlen) {
    assert(ctx != NULL);
    // Encyption size is nondeterministic but fixed. See ec_override.c for details.
    size_t max_required_size = max_encryption_size();

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

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

    return 1;
}