Earlier quoted context omitted.
It doesn't. It's not a buffer overflow issue.
It's an uninitialized read, and PolarSSL is actually also proven to lack uninitialized reads. It's just that asn1_get_sequence_of was not included in verification (as it is unreachable in verified configuration).
Which shows you the limit of verification toolsets vs. a verifying compiler. To verify that the code is 100% free of uninitialized reads or uses-after-free the static analyzer would have to scan through all possible permutations.
Sure, you can get very close to 100% in practice, but even if you're fine with this level of guarantee, the amount of discipline and cognitive overhead required for doing that in C makes Rust's learning seem like a piece of cake.