int EVP_CIPHER_CTX_ctrl()

in source/evp_override.c [468:490]

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

int EVP_CIPHER_CTX_ctrl(EVP_CIPHER_CTX *ctx, int type, int arg, void *ptr) {
    if (type == EVP_CTRL_GCM_SET_IVLEN || type == EVP_CTRL_AEAD_SET_IVLEN) {
        assert(ctx->iv_set == false);
        /* iv length must be positive */
        assert(arg > 0);
        ctx->iv_len = arg;
    }

    /* Only legal when encrypting data. */
    assert(IMPLIES(type == EVP_CTRL_GCM_GET_TAG, ctx->encrypt == 1));
    assert(IMPLIES(type == EVP_CTRL_GCM_GET_TAG, ctx->data_processed == true));
    /* Need to be able to write taglen (arg) bytes to buffer ptr. */
    assert(IMPLIES(type == EVP_CTRL_GCM_GET_TAG, __CPROVER_w_ok(ptr, arg)));

    /* Only legal when decrypting data. */
    assert(IMPLIES(type == EVP_CTRL_GCM_SET_TAG, ctx->encrypt == 0));
    /* Need to be able to write taglen (arg) bytes to buffer ptr. */
    assert(IMPLIES(type == EVP_CTRL_GCM_SET_TAG, __CPROVER_w_ok(ptr, arg)));

    int rv;
    __CPROVER_assume(rv == 0 || rv == 1);
    return rv;
}