From fc72ef83f718683de25497d7db6bfc515136e018 Mon Sep 17 00:00:00 2001 From: Daniele Lacamera Date: Fri, 31 Jul 2026 15:22:00 +0200 Subject: [PATCH] md5: remove unreachable len operand in wc_Md5Update Premise: md5.c:345 `if (md5 == NULL || (data == NULL && len > 0)) return BAD_FUNC_ARG;` establishes !(data == NULL && len > 0), i.e. data != NULL || len == 0. Claim: md5.c:361 `if (data == NULL && len == 0)` -- the `len == 0` operand. Proof: under the left conjunct data == NULL, the premise forces len == 0. len is word32, so !(len > 0) is exactly len == 0 -- no signed wraparound case to consider. Neither data nor len is written between :345 and :361. The operand is invariantly true when evaluated and its independence pair is unreachable. Scope: the intervening code is the WOLFSSL_ASYNC_CRYPT && WC_ASYNC_ENABLE_MD5 block (:349-355), which may return early but writes neither variable, and the buffLen range check (:358). The argument holds in all four combinations of those two macros. Evidence: llvm-cov MC/DC records this condition's pair as uncovered (reports/md5/GAPS.md row 361:9:361:33:1); it is the sole residual holding md5.c at 12/13. Proof check: gcc does not fold this (it does not propagate the correlation between the entry guard's two operands across the branch), so the implication was machine-checked instead: with data == NULL held true, all 2^32 word32 values of len were enumerated and every one that passes the :345 guard has len == 0. Zero counterexamples -- exhaustive, not sampled. --- wolfcrypt/src/md5.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/wolfcrypt/src/md5.c b/wolfcrypt/src/md5.c index 9e6c22cbd3..f6c72d3118 100644 --- a/wolfcrypt/src/md5.c +++ b/wolfcrypt/src/md5.c @@ -358,8 +358,8 @@ int wc_Md5Update(wc_Md5* md5, const byte* data, word32 len) if (md5->buffLen >= WC_MD5_BLOCK_SIZE) return BUFFER_E; - if (data == NULL && len == 0) { - /* valid, but do nothing */ + if (data == NULL) { + /* len is 0 here: valid, but do nothing */ return 0; }