AstraVer Toolset » Deductive Verification Tools for Linux Kernel

static int parse_x509_signatureValue(const u8 *buf, u16 len,
                                     const _alg_id *sig_alg, u16 *eaten)
{
        int ret;

        ...

        /*@ calls parse_sig_ecdsa, parse_sig_generic; @*/
        ret = sig_alg->parse_sig(buf, len, eaten);
        if (ret) {
                ERROR_TRACE_APPEND(__LINE__);
                goto out;
        }

        ret = 0;

out:
        return ret;
}