The PhD memoir “The C standard formalized in Coq” (Robbert Krebbers) arrived by post todaypic.twitter.com/88gEyZR01u
You can add location information to your Tweets, such as your city or precise location, from the web and via third-party applications. You always have the option to delete your Tweet location history. Learn more
@spun_off @ch3root There is no license for i==j to evaluate inconsistently when UB was not invoked.
@RichFelker @spun_off DR 260 contradicts the text of the standard in a fundamental way so figuring which parts of the std still hold and\
@RichFelker @spun_off which don't hold is non-trivial. At least it took me some time. So asking if comparison of integers is still sane\
@RichFelker @spun_off seems quite natural to me. (And he found a bug in the gcc in it after all!) But the text implies that the decision is\
@RichFelker @spun_off arbitrary. Like:
- Let's break integer comparison.
- No, that's too much.
@ch3root @RichFelker It is arbitrary! This is like GCC backtracking on UB from using uninitialized memory between 4.4.3 and 4.4.7, or…
@ch3root @RichFelker backtracking from pointer comparison optimizations since https://lwn.net/Articles/278137/ … . They have no idea what they're doing
@ch3root @RichFelker To them it's a game and benchmarks are the scoring system.
@spun_off @RichFelker Are you saying that aliasing analysis is not needed at all? Go tell it @bmastenbrook.
@RichFelker @spun_off @ch3root right, if we assume that intptr_t is long, and so the printf formats are correct ...
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.