link to compcert

[web.git] / ralf / _posts / 2018-07-24-pointers-and-bytes.md

diff --git a/ralf/_posts/2018-07-24-pointers-and-bytes.md b/ralf/_posts/2018-07-24-pointers-and-bytes.md
index a51fb48652b79c9adbebe92fe018407ecca1249e..3211346c9f705afd635aeef8ab739b3fb2b20246 100644 (file)
--- a/ralf/_posts/2018-07-24-pointers-and-bytes.md
+++ b/ralf/_posts/2018-07-24-pointers-and-bytes.md
@@ -111,7 +111,7 @@ So, what *is* a pointer?
 I don't know the full answer to this.
 In fact, this is an open area of research.
 
-Here's a simple proposal (in fact, this is the model used in my [RustBelt work]({{ site.baseurl }}{% post_url 2017-07-08-rustbelt %}), and it is also how [miri](https://github.com/solson/miri/) implements pointers):
+Here's a simple proposal (in fact, this is the model of pointers used in [CompCert](https://hal.inria.fr/hal-00703441/document) and my [RustBelt work]({{ site.baseurl }}{% post_url 2017-07-08-rustbelt %}), and it is also how [miri](https://github.com/solson/miri/) implements pointers):
 A pointer is a pair of some kind of ID uniquely identifying the *allocation*, and an *offset* into the allocation.
 Adding/subtracting an integer to/from a pointer just acts on the offset, and can thus never leave the allocation.
 Subtracting a pointer from another is only allowed when both point to the same allocation (matching [C++](https://timsong-cpp.github.io/cppwp/n4140/expr.add#6)).[^2]
@@ -203,6 +203,7 @@ Using `Uninit` instead of an arbitrary bit pattern means miri can, in a single e
 We have seen that pointers can be different even when they point to the same address, and that a byte is more than just a number in `0..256`.[^4]
 With this, I think we are ready to look at a first draft of my "2018 memory model" (working title ;) -- in the next post. :)
 
+Thanks to @rkruppe and @nagisa for help in finding arguments for why `Uninit` is needed.
 If you have any questions, feel free to [ask in the forums](https://internals.rust-lang.org/t/pointers-are-complicated-or-whats-in-a-byte/8045)!
 
 [^4]: And just to be clear, I am talking about a pointer or byte in the model of an optimized *programming language* here.  When modeling hardware, everything is different.