File: mldsa/src/sign.c, in mld_sign:

c
ret = mld_sign_signature(sm, smlen, sm + MLDSA_CRYPTO_BYTES, mlen, ctx,
                         ctxlen, sk, context);
*smlen += mlen;
return ret;


If mld_sign_signature fails, it sets *siglen = 0. Then *smlen += mlen makes *smlen = mlen on failure. The CBMC contract says the function
should return *smlen == MLDSA_CRYPTO_BYTES + mlen on success, but doesn't constrain *smlen on failure. However, returning a non-zero
*smlen on failure could confuse callers into thinking there's valid data in the buffer. The mld_sign_open counterpart does set *mlen = 0
on failure.

Severity: Low (robustness). Consider setting *smlen = 0 on error for defensive consistency.