Hack of the day: Integer comparison can be used to compare positive IEEE floats. I need this bc there's no atomicMax() for floats in CUDA.pic.twitter.com/RMsQrfALEj
-
It depends on the C std. Type punning via unions is only legal in >= C99. The type punning in test2 is illegal everywhere
Yes. But this does not seem to be what bothers ESBMC here. It happily verifies this two test cases. But -0 == +0 in IEEE fp, so CBMC fails.pic.twitter.com/T37y04ZXwx
-
-
I wonder why they fail, then. I think they're not assuming IEEE floats.
-
They fail in CBMC because CBMC _is_ assuming IEEE floats. -0 == +0 is true with IEEE floats, but their bit pattern differ.
- Show replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.