See [this page](http://blog.frama-c.com/index.php?post/2013/05/02/nearbyintf1) for a correct implementation of `round`.