user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

expand explanation of how we treat validity invariants

Browse source
This commit is contained in:
Ralf Jung 2019-05-20 09:32:01 +02:00
parent f761450aba
commit df36c2bb7d
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
README.md
View file

@ -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.