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
I tried to prove this with ESBMC first, but apparently ESBMC is not using IEEE floats to represent float values. Which C model checker does?
-
-
Well. Any C checker will tell you your programs behavior is undefined.
-
jfyi: I've now tested two implementations of formal tests for this: mine and the one by
@rrika9. Both pass in CBMC and fail in ESBMC.pic.twitter.com/dJAZyAXk9H
- Show replies
New conversation -
-
-
CBMC assumes IEEE floats. http://rise4fun.com/Z3/HXi2 https://gist.github.com/rrika/785ae6ee09aa92009f495e3b65a08c18 …
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.