extend footnote on other tools

[web.git] / personal / _posts / 2025-12-22-miri.md

diff --git a/personal/_posts/2025-12-22-miri.md b/personal/_posts/2025-12-22-miri.md
index 272f9c3e0944e4222e74c908128a5f15f67fa30a..d1c4dd3f0f69839adaa0a411fcf9e1e15444d874 100644 (file)
--- 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.<!-- MORE -->[^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.