Page History

...

Tool

Version

Checker

Description

Include Page

	Astrée_V
	Astrée_V

float-division-by-zero

Partially 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 D

Partially implemented

Parasoft C/C++test

Include Page

	Parasoft_V
	Parasoft_V

BD-PB-ZERO, MISRA2004-10_2_b, MISRA2004-10_2_c, MISRA2004-10_2_d

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

Implemented

Parasoft Insure++ Runtime analysis

Polyspace Bug Finder

R2016a

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