Frama-C can be used in &quot;interpreter mode&quot; where it acts like a checking C interpreter. It then catches a superset of the bugs that would be caught by Valgrind &#x2F; ASan &#x2F; UBSan. On the other hand it is slower and harder to use than those tools.