UB post: clarify

diff --git a/ralf/_posts/2017-07-14-undefined-behavior.md b/ralf/_posts/2017-07-14-undefined-behavior.md
index 46356689dfa90848d28f5d5b387758fc334bc2b3..851f737909324a3cb7d6d5d710ece80e84f44e88 100644 (file)
--- a/ralf/_posts/2017-07-14-undefined-behavior.md
+++ b/ralf/_posts/2017-07-14-undefined-behavior.md
@@ -52,6 +52,11 @@ However, if they *do* alias, that would violate the effective type restriction,
 As we have seen, in both of the possible cases, the reordering is correct; the compiler is thus free to perform the transformation.
 
 Undefined behavior moves the burden of proving the correctness of this optimization from the compiler to the programmer.
 As we have seen, in both of the possible cases, the reordering is correct; the compiler is thus free to perform the transformation.
 
 Undefined behavior moves the burden of proving the correctness of this optimization from the compiler to the programmer.

+In the example above, what the "effective type" rule really means is that every single memory read of a `float` comes with a *proof obligation*:
+The programmer has to show that that the last write to this memory actually happened through a `float` pointer (baring some exceptions around union and character pointers).
+Similarly, the (in)famous rule that [signed integer overflow is undefined behavior](https://stackoverflow.com/questions/16188263/is-signed-integer-overflow-still-undefined-behavior-in-c) means that every single arithmetic operation on signed integers comes with the proof obligation that this operation will never, ever, overflow.
+The compiler performs its optimization under the assumption that the programmer actually went through the effort and convinced itself that this is the case.
+

 Considering that the compiler can only be so smart, this is a great way to justify optimizations that would otherwise be difficult or impossible to perform.
 Unfortunately, it is often not easy to say whether a program has undefined behavior or not -- after all, such an analysis being difficult is the entire reason compilers have to rely on UB to perform their optimizations.
 Furthermore, while C compilers are happy to exploit the fact that a particular program *has* UB, they do not provide a way to test that executing a program *does not* trigger UB.
 Considering that the compiler can only be so smart, this is a great way to justify optimizations that would otherwise be difficult or impossible to perform.
 Unfortunately, it is often not easy to say whether a program has undefined behavior or not -- after all, such an analysis being difficult is the entire reason compilers have to rely on UB to perform their optimizations.
 Furthermore, while C compilers are happy to exploit the fact that a particular program *has* UB, they do not provide a way to test that executing a program *does not* trigger UB.


@@ -89,4 +94,6 @@ It is with such considerations in my mind that I have previously written about [
 Coming up next on this channel:  During my [internship]({{ site.baseurl }}{% post_url 2017-05-23-internship-starting %}), I am working on such a specification.
 My ideas are concrete enough now that I can write down a draft, which I will share with the world to see what the world thinks about it.
 
 Coming up next on this channel:  During my [internship]({{ site.baseurl }}{% post_url 2017-05-23-internship-starting %}), I am working on such a specification.
 My ideas are concrete enough now that I can write down a draft, which I will share with the world to see what the world thinks about it.
 

-**Uodate:** [Writing down has happened]({{ site.baseurl }}{% post_url 2017-07-17-types-as-contracts %}).
+**Update:** [Writing down has happened]({{ site.baseurl }}{% post_url 2017-07-17-types-as-contracts %}).
+
+**Update:** Clarified "Shifting Responsibility".