Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.

...

Tool

Version

Checker

Description

Astrée
Include Page
Astrée_V
Astrée_V
CERT.FLP.3float-division-by-zeroPartially checked
Compass/ROSE

 

 

Could detect violations of this rule by ensuring that floating-point operations are surrounded by feclearexcept() and fetestexcept(). It would need to look for type conversions to float or double, divisions (by a number not known to be nonzero), and multiplication. It may be wisest to apply this to all floating-point operations in general

LDRA tool suite
Include Page
LDRA_V
LDRA_V
43 DPartially implemented
Parasoft C/C++test9.5BD-PB-ZERO, MISRA2004-10_2_{b,c,d}Partially implemented
Parasoft Insure++  Runtime analysis
Polyspace Bug FinderR2016a

Float conversion overflow

Float overflow

Invalid use of standard library floating point routine

Float division by zero

Overflow when converting between floating point data types

Overflow from operation between floating points

Wrong arguments to standard library function

Dividing floating point number by zero

...