Because it takes a lot of effort. Google Frama-C. On the flip side, it can express not just memory safety constraints, but also correctness proofs.

In this case it's not about Frama-C or similar tools though, see your sibling comments about the caveats.

Arguably, generating verified C from a low-level focused subset of F* (Low*, used in the HACL project) is close enough to count as a "similar tool".