X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/709252ab99debf5fdde52aa0972466a8e4af8b1c..334aed819b1926247741d786ed21b0c43cdf71c4:/ralf/_posts/2017-07-14-undefined-behavior.md?ds=sidebyside diff --git a/ralf/_posts/2017-07-14-undefined-behavior.md b/ralf/_posts/2017-07-14-undefined-behavior.md index e93a608..77e7315 100644 --- a/ralf/_posts/2017-07-14-undefined-behavior.md +++ b/ralf/_posts/2017-07-14-undefined-behavior.md @@ -39,7 +39,7 @@ This could be the end of the game: No alias information, no way to verify our a ## Shifting responsibility -However, it turns out that compilers writers consider these optimizations important enough that they came up with an alternative solution: +However, it turns out that compiler writers consider these optimizations important enough that they came up with an alternative solution: Instead of having the compiler verify such assumptions, they declared the programmer responsible. For example, the C standard says that memory accesses have to happen with the right "effective type": If data was stored with a `float` pointer, it must not be read with an `int` pointer. @@ -87,4 +87,6 @@ Such a specification would describe the additional state that is needed at run-t It is with such considerations in my mind that I have previously written about [miri as an executable specification]({{ site.baseurl }}{% post_url 2017-06-06-MIR-semantics %}). 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. -I have a draft ready now, and I will share it with the world to see what the world thinks about it. +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 %}).