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
@RichFelker @spun_off @ch3root however (void*)x == (void*)y, assuming that casting from uintptr_t to void* is just looking up ptr in array.
@RichFelker @spun_off @ch3root Also, (uintptr_t)NULL != 0 and (void*)(uintptr_t)0 isn't necessarily NULL.
@BRIAN_____ (void*)(uintptr_t)0 has to compare == to any other null pointer, because it is a null pointer. NULL is a null ptr—C99 6.3.2.3:4
@spun_off Only when `0` is in a pointer context. (uintptr_t)0 isn't a pointer context.
@BRIAN_____ But (uintptr_t)0 is 0, no?
@BRIAN_____ @RichFelker @spun_off Yes, I can imagine this. I think it's unlikely, in practice, for a cast to uintptr_t but comparisons of\
@BRIAN_____ @RichFelker @spun_off pointers are definitely behave strangely.
@BRIAN_____ @RichFelker @spun_off E.g. p==q is unstable -- it could be false now and true later even if p and q are not changed\
@BRIAN_____ @RichFelker @spun_off (due to lost provenance info).
@BRIAN_____ @RichFelker @spun_off Or there could be pointers p, q, r such that r == p, r == q, p != q.
@BRIAN_____ @RichFelker @spun_off Probably most wtf moments are in https://gcc.gnu.org/bugzilla/show_bug.cgi?id=61502 … and https://gcc.gnu.org/bugzilla/show_bug.cgi?id=65752 …
@BRIAN_____ @RichFelker @spun_off BTW Robbert which reported https://gcc.gnu.org/bugzilla/show_bug.cgi?id=65752 … is that Robbert.
@BRIAN_____ @spun_off But to iterate @RichFelker's point: after you convert your pointers to integers all these problems go away.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.