Frama-C can be used in "interpreter mode" where it acts like a checking C interpreter. It then catches a superset of the bugs that would be caught by Valgrind /

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