mirror of
https://github.com/wolfSSL/wolfssl.git
synced 2026-08-19 07:23:27 +02:00
Daniele Lacamera
fc72ef83f7
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.