From df36c2bb7d6a71d3fe420e1aba9a0bd0655e9758 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 20 May 2019 09:32:01 +0200 Subject: [PATCH] expand explanation of how we treat validity invariants --- README.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 22eb41f94900..ae2f5f506f16 100644 --- a/README.md +++ b/README.md @@ -23,9 +23,11 @@ Be aware that Miri will not catch all possible errors in your program, and cannot run all programs: * There are still plenty of open questions around the basic invariants for some - types and when these invariants even have to hold, so if you program runs fine - in Miri right now that is by no means a guarantee that it is UB-free when - these questions get answered. + types and when these invariants even have to hold. Miri tries to avoid false + positives here, so if you program runs fine in Miri right now that is by no + means a guarantee that it is UB-free when these questions get answered. In + particular, Miri does currently not check that integers are initialized or + that references point to valid data. * If the program relies on unspecified details of how data is laid out, it will still run fine in Miri -- but might break (including causing UB) on different compiler versions or different platforms.