int EVP_PKEY_sign()

in source/evp_override.c [174:201]

• 23 lines of code
• 5 McCabe index (conditional complexity)

int EVP_PKEY_sign(EVP_PKEY_CTX *ctx, unsigned char *sig, size_t *siglen, const unsigned char *tbs, size_t tbslen) {
    assert(evp_pkey_ctx_is_valid(ctx));
    assert(ctx->is_initialized_for_signing == true);
    assert(siglen);
    assert(!sig || (*siglen >= max_signature_size() && __CPROVER_w_ok(sig, *siglen)));
    assert(tbs);
    assert(__CPROVER_r_ok(tbs, tbslen));

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

    // Signature size is nondeterministic but fixed. See ec_override.c for details.
    size_t max_required_size = max_signature_size();

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

    return 1;
}