From 7fe1df6b1c7d960c8d336aa1e513d9a08fd21e75 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 24 Jul 2018 17:38:36 +0200 Subject: [PATCH] link to compcert --- personal/_posts/2018-07-24-pointers-and-bytes.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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] -- 2.30.2