int EVP_DecryptUpdate()

in source/evp_override.c [593:622]

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

int EVP_DecryptUpdate(EVP_CIPHER_CTX *ctx, unsigned char *out, int *outl, const unsigned char *in, int inl) {
    assert(ctx != NULL);
    assert(ctx->data_processed == false);
    int rv;
    __CPROVER_assume(rv == 0 || rv == 1);
    if (out == NULL) {  // specifying aad
        return rv;
    }
    size_t out_size;
    __CPROVER_assume(out_size >= 0);
    if (ctx->cipher) {
        if (ctx->padding) {
            __CPROVER_assume(out_size <= inl);
        }
    } else {
        __CPROVER_assume(out_size <= inl);
        ctx->data_remaining = inl - out_size;
    }
    /*
     * This check is redundant with the following __CPROVER_w_ok.
     * __CPROVER_w_ok is a macro for __CPROVER_w_ok primitive, which
     * should return true if out is writable upt to out_size bytes;
     * however, __CPROVER_w_ok has been replaced by a simple nullness check for now.
     * Thus, we also include an additional check using __CPROVER_OBJECT_SIZE.
     */
    assert(__CPROVER_OBJECT_SIZE(out) >= out_size);
    assert(__CPROVER_w_ok(out, out_size));
    *outl = out_size;
    return rv;
}