Invalid Use of Standard Library Floating Point Routines

Polyspace^® Code Prover™ performs the Invalid Use of Standard Library Routine check on standard library routines to determine if their arguments are valid. The check works differently for memory routines, floating-point routines or string routines because their arguments can be invalid in different ways. This topic describes how the check works for standard library floating-point routines.

For more information on the check, see Invalid use of standard library routine.

What the Check Looks For

The Invalid Use of Standard Library Routine check sequentially looks for the following issues in use of floating-point routines.

• Domain error: A domain error occurs if the arguments of the function are invalid. The definition of invalid argument varies based on whether you allow non-finite floats or not. If you allow non-finite floats but:

  • Specify that you must be warned about NaN results, a domain error occurs if the function returns NaN and the arguments themselves are not NaN.

  • Specify that NaN results must be forbidden, a domain error occurs if the function returns NaN or the arguments themselves are NaN.

  For details, see NaNs (-check-nan).

  The check works in almost the same way as the check Invalid operation on floats. The Invalid Use of Standard Library Routine check works on standard library functions while the Invalid Operation on Floats check works on numerical operations involving floating-point variables.

• Overflow error: An overflow error occurs if the result of the function overflows. The definition of overflow varies based on whether you allow non-finite floats and based on the rounding modes you specify. If you allow non-finite floats but specify that you must be warned about infinite results, an overflow error occurs if the function returns infinity and the arguments themselves are not infinity. For details, see Infinities (-check-infinite).

  The check works in the same way as the check Overflow. The Invalid Use of Standard Library Routine check works on standard library functions while the Overflow check works on numerical operations involving floating-point variables.

• Invalid pointer argument: For functions such as frexp that take pointer arguments, the verification checks if it is valid to dereference the pointer. For instance, the pointer is not NULL or does not point outside allowed bounds.

For more information on analysis options, see the documentation for Polyspace Code Prover or Polyspace Code Prover Server™.

The check looks for these errors in sequence.

• If the check finds a definite domain error, it does not look for the overflow error.

• If the check finds a possible domain error, it looks for the overflow error only for the execution paths where the domain error does not occur.

The check for each error itself can consist of multiple conditions, which are also checked in sequence. Each check is performed only for those execution paths where the previous check passes.

Single-Argument Functions Checked

The Invalid Use of Standard Library Routine check covers the following routines, their single-precision versions with suffix f (if they have one) and their long double versions with suffix l. The check works in exactly the same way for C and C++ code.

• acos

• acosh

• asin

• asinh

• atan

• atanh

• ceil

• cos

• cosh

• exp

• exp2

• expm1

• fabs

• floor

• log

• log10

• log1p

• logb

• round

• sin

• sinh

• sqrt

• tan

• tanh

• trunc

• cbrt

Functions with Multiple Arguments

The Invalid Use of Standard Library Routine check covers the following routines, their single-precision versions with suffix f (if they have one) and their long double versions with suffix l. The check works in exactly the same way for C and C++ code.

• atan2

• fdim

• fma

• fmax

• fmin

• fmod

• frexp

• hypot

• ilogb

• ldexp

• modf

• nextafter

• nexttoward

• pow

• remainder