CBMC 5.3 and prior: bug in encoding of floating-point division
153 views
Skip to first unread message
Daniel Kroening
Feb 17, 2016, 9:19:20 AM2/17/16
to cpr...@googlegroups.com
Dear everyone,
as part of our routine QA process we have found an issue with our model
of floating-point divide. In a few cases where very large numbers are
divided by very small (subnormal) numbers, zero is returned rather than
infinity. Given that the range of numbers required to trigger this
issue we do not believe that it will have a major impact on users but
please contact us if this is an issue for you. The patch has been
applied to the subversion trunk and will be in the next release.
With best regards,
Daniel
as part of our routine QA process we have found an issue with our model
of floating-point divide. In a few cases where very large numbers are
divided by very small (subnormal) numbers, zero is returned rather than
infinity. Given that the range of numbers required to trigger this
issue we do not believe that it will have a major impact on users but
please contact us if this is an issue for you. The patch has been
applied to the subversion trunk and will be in the next release.
With best regards,
Daniel
Reply all
Reply to author
Forward
0 new messages