Mercury Bugs - mercury
View Issue Details
0000471mercuryBugpublic2018-09-22 14:012018-09-22 14:01
Reporterwangp 
Assigned To 
PrioritynormalSeverityminorReproducibilityalways
StatusnewResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0000471: float rounding
Descriptionfloat.round_to_int and math.round are implemented with
    floor(X + 0.5)

There are problems with very large floats that behave as integers, e.g.
    round(8333333333388609.0) -> 8333333333388610.0

or when the fractional part is the predecessor of 0.5, e.g.
    round_to_int(0.49999999999999994) -> 1

See http://blog.frama-c.com/index.php?post/2013/05/02/nearbyintf1

I think no real programs would intentionally depend on the current behaviour so we should be free to fix the implementation.

---

BTW {ceiling,floor,round,truncate}_to_int should specify the behaviour if the value would overflow the result type [or if the input is NaN]. But that's only one aspect of overflow handling that we don't do yet.
TagsNo tags attached.
Attached Files

There are no notes attached to this issue.

Issue History
2018-09-22 14:01wangpNew Issue