add MoSeL paper

[web.git] / ralf / _posts / 2017-07-14-undefined-behavior.md

diff --git a/ralf/_posts/2017-07-14-undefined-behavior.md b/ralf/_posts/2017-07-14-undefined-behavior.md
index 851f737909324a3cb7d6d5d710ece80e84f44e88..8176aaf552e60f7f272fd25936e4d5df564fbdd3 100644 (file)
--- a/ralf/_posts/2017-07-14-undefined-behavior.md
+++ b/ralf/_posts/2017-07-14-undefined-behavior.md
@@ -62,6 +62,8 @@ Unfortunately, it is often not easy to say whether a program has undefined behav
 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.
 It also turns out that programmers' intuition often [does not match what the compiler does](https://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html), which leads to miscompilations (in the eye of the programmer) and sometimes to security [vulnerabilities](https://lwn.net/Articles/342330/).
 As a consequence, UB has a pretty bad reputation.
+(The fact that most people will not expect an innocent-looking `+` operation to come with subtle proof obligations concerning overflow probably also plays a role in this.
+In other words, this is also an API design problem.)
 
 There are various sanitizers that watch a program while it is being executed and try to detect UB, but they are not able to catch all possible sources of UB.
 Part of the reason this is so hard is that the standard has not been written with such sanitizers in mind.