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 The derivation of integers i and j is well-defined for a given impl, and so is compar of ints. Either they are == or not.
@RichFelker @spun_off @ch3root Consider an implementation that implements (uintptr_t) casting in the following way:
@RichFelker @spun_off @ch3root
uintptr_t x = (uintptr_t)p; // x := 1
uintptr_t y = (uintptr_t)p; // y := 2, y != x.
@BRIAN_____ @spun_off @ch3root I think it's clear that the intent of impl-defined conversion is that it be a function of the value...
@BRIAN_____ @spun_off @ch3root ...i.e. that multiple conversions of the same value produce the same result.
@BRIAN_____ @spun_off @ch3root Even if this weren't a requirement, the ABI already defines the impl-defined conversion here.
@BRIAN_____ @spun_off @ch3root + Footnote 67 says "intended to be consistent with the addressing structure of the execution environment."
@RichFelker @spun_off @ch3root That's actually standards speak arguing against your point. "Let's add a meaningless footnote and move on."
@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.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.