int i2d_ECDSA_SIG()

in source/ec_override.c [334:354]

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

int i2d_ECDSA_SIG(const ECDSA_SIG *sig, unsigned char **pp) {
    assert(ecdsa_sig_is_valid(sig));
    assert(pp != NULL);
    assert(*pp != NULL);                                // Assuming is never called with *pp == NULL
    assert(__CPROVER_w_ok(*pp, max_signature_size()));  // *pp has enough space for the signature

    // Documentation says 0 is returned on error, but OpenSSL implementation returns -1
    // To be safe, we return a number <= 0
    if (nondet_bool()) {
        int error_code;
        __CPROVER_assume(error_code <= 0);
        return error_code;
    }

    int sig_len;
    __CPROVER_assume(0 < sig_len && sig_len <= max_signature_size());
    write_unconstrained_data(*pp, sig_len);
    *pp += sig_len;  // Unclear from the documentation if *pp should really be incremented

    return sig_len;
}