Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.
Comment: Added PC-lint Plus to Automated Detection Table

...

Tool

Version

Checker

Description

Astrée
Include Page
Astrée_V
Astrée_V
float-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++test
Include Page
Parasoft_V
Parasoft_V

CERT_C-FLP03-a
CERT_C-FLP03-b
CERT_C-FLP03-c
CERT_C-FLP03-d

Avoid division by zero
Avoid implicit conversions from wider to narrower floating type
Avoid implicit conversions from narrower to wider floating type
Avoid implicit conversions of floating point numbers from wider to narrower floating type

Parasoft Insure++

Runtime analysis
PC-lint Plus

Include Page
PC-lint Plus_V
PC-lint Plus_V

736, 9120, 9227

Assistance provided

Polyspace Bug Finder

Include Page
Polyspace Bug Finder_V
Polyspace Bug Finder_V

CERT C: Rec. FLP03-C


Checks for:

  • Float conversion overflow
  • Float overflow
  • Float division by zero

Rec. partially covered.

...