From: Ralf Jung Date: Tue, 24 Jul 2018 15:38:36 +0000 (+0200) Subject: link to compcert X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/7f664f1f429187a9892d497a664cc0560b8b1443?ds=inline link to compcert --- diff --git a/personal/_posts/2018-07-24-pointers-and-bytes.md b/personal/_posts/2018-07-24-pointers-and-bytes.md index 8338de4..3211346 100644 --- a/personal/_posts/2018-07-24-pointers-and-bytes.md +++ b/personal/_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]