X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/67e0db9b2a3d2d66193b91f4189804dc93676d93..e4d2676d0304ae068a925de5f052626463c12c31:/personal/_posts/2017-07-14-undefined-behavior.md

diff --git a/personal/_posts/2017-07-14-undefined-behavior.md b/personal/_posts/2017-07-14-undefined-behavior.md
index 851f737..8176aaf 100644
--- a/personal/_posts/2017-07-14-undefined-behavior.md
+++ b/personal/_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.