const: clarify and typo

[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 adf82bd8d8e724b2a4b2597113207798e4cd1603..05690b3a6e3fb88860c4adb39025f7b605b30cde 100644 (file)
--- a/ralf/_posts/2018-07-24-pointers-and-bytes.md
+++ b/ralf/_posts/2018-07-24-pointers-and-bytes.md
@@ -137,7 +137,8 @@ However, this simple model starts to fall apart once you consider pointer-intege
 In miri, casting a pointer to an integer does not actually do anything, we now just have an integer variable (i.e., its *type* says it is an integer) whose *value* is a pointer (i.e., an allocation-offset pair).
 However, multiplying that "integer" by 2 leads to an error, because it is entirely unclear what it means to multiply such an abstract pointer by 2.
 
 In miri, casting a pointer to an integer does not actually do anything, we now just have an integer variable (i.e., its *type* says it is an integer) whose *value* is a pointer (i.e., an allocation-offset pair).
 However, multiplying that "integer" by 2 leads to an error, because it is entirely unclear what it means to multiply such an abstract pointer by 2.
 

-This is the most lazy thing to do, and we do it because it is not clear what else to do -- in our abstract machine, there is no single coherent "address space" that all allocations live in, that we could use to map every pointer to a distinct integer.
+This is the most lazy thing to do, and we do it because it is not clear what else to do (other than not supporting these casts at all -- but this way, miri can run more programs).
+In our abstract machine, there is no single coherent "address space" that all allocations live in, that we could use to map every pointer to a distinct integer.

 Every allocation is just identified by an (unobservable) ID.
 We could now start to enrich this model with extra data like a base address for each allocation, and somehow use that when casting an integer back to a pointer... but that's where it gets really complicated, and anyway discussing such a model is not the point of this post.
 The point it to discuss the *need* for such a model.
 Every allocation is just identified by an (unobservable) ID.
 We could now start to enrich this model with extra data like a base address for each allocation, and somehow use that when casting an integer back to a pointer... but that's where it gets really complicated, and anyway discussing such a model is not the point of this post.
 The point it to discuss the *need* for such a model.