From: Ralf Jung Date: Tue, 24 Jul 2018 14:39:39 +0000 (+0200) Subject: tweak X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/f749955ae1555b01cf4ad0e82ae3fd90d13044b6?ds=inline;hp=70c890b37d1ce56cae160189c065aefb1de56704 tweak --- diff --git a/ralf/_posts/2018-07-24-pointers-and-bytes.md b/ralf/_posts/2018-07-24-pointers-and-bytes.md index 61ecc14..defc2ec 100644 --- a/ralf/_posts/2018-07-24-pointers-and-bytes.md +++ b/ralf/_posts/2018-07-24-pointers-and-bytes.md @@ -43,7 +43,7 @@ First of all, it is not allowed to perform pointer arithmetic (like `&x[i]` does Our program violates this rule: `x[i]` is outside of `x`, so this is undefined behavior. To be clear: Just the *computation* of `x_ptr` is already UB, we don't even get to the part where we want to *use* this pointer![^1] -[^1]: It turns out that `y-x` is also undefined behavior because [one may only subtract pointers into the same allocation](https://timsong-cpp.github.io/cppwp/n4140/expr.add#6). However, we could use `i = ((size_t)y - (size_t)x)/sizeof(int)` to work around that. +[^1]: It turns out that `i = y-x` is *also* undefined behavior because [one may only subtract pointers into the same allocation](https://timsong-cpp.github.io/cppwp/n4140/expr.add#6). However, we could use `i = ((size_t)y - (size_t)x)/sizeof(int)` to work around that. But we are not done yet: This rule has a special exception that we can exploit to our advantage. If the arithmetic ends up computing a pointer *just past* the end of an allocation, that computation is fine. @@ -199,8 +199,10 @@ Using `Uninit` instead of an arbitrary bit pattern means miri can, in a single e ## Conclusion -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`. +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. :) +[^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. + #### Footnotes