From: Ralf Jung Date: Tue, 23 Dec 2025 09:29:47 +0000 (+0100) Subject: extend footnote on other tools X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/e489f258dae5b1ffd3fa4d2962eb6ecf2d89ce89?hp=f9727c918ea8b82a1ef1a109c6e9fbe78e1c0e7b extend footnote on other tools --- diff --git a/personal/_posts/2025-12-22-miri.md b/personal/_posts/2025-12-22-miri.md index 272f9c3..d1c4dd3 100644 --- a/personal/_posts/2025-12-22-miri.md +++ b/personal/_posts/2025-12-22-miri.md @@ -13,7 +13,7 @@ This means it can find bugs in your unsafe code where you failed to uphold requi Miri's claim to fame is that it is a practical tool that can find *all de-facto Undefined Behavior in deterministic Rust programs*. To my knowledge, no other freely available tool can claim this---for any language.[^relwork] -[^relwork]: Please let me know if there is such a tool and I just missed it! +[^relwork]: Please let me know if there is such a tool and I just missed it! The paper discusses why sanitizers and valgrind, while being immensely useful tools, still miss some UB. I just know of one commercial tool that can make similar claims to Miri, the "TrustInSoft Analyzer". It requires a license, so I can't say how good its coverage of the C standard is; in particular, it would be interesting to compare what GCC and clang think is UB with what the tool thinks. In Miri, we spend a lot of time discussing with compiler folks to ensure we all have a shared understanding of what is and is not UB. In principle, this should not be needed in C since it has a standard; in practice, the standard can [diverge pretty far](https://dl.acm.org/doi/10.1145/2908080.2908081) from what programmers expect and from what compilers implement. We can only talk about *de-facto UB* because Rust has not yet stabilized its definition of Undefined Behavior. In lieu of that, we carefully check what the compiler does to ensure, to the best of our abilities, that all the UB which a Rust program can encounter *today* is caught by Miri.