Main Content

Fix Polyspace Overapproximations on Standard Library Math Functions

Issue

In your verification results, a standard library math function does not behave as expected.

For instance, the statement assert(isinf(x)) does not constrain the value of x to positive or negative infinity in subsequent statements.

Cause

If Polyspace® cannot find the math function definitions, the verification uses Polyspace implementations of the standard library math functions.

In some cases, the Polyspace implementation of the function might not match the function specification. Note that in such cases, the Polyspace implementation overapproximates the function behavior. For instance, following the statement assert(isinf(x)), the range of values of x include positive and negative infinity. Therefore, such behavior does not lead to green checks for operations that can cause run-time errors.

Solution

Explicitly provide the path to your compiler’s native header files so that the verification uses your compiler’s implementations of the functions. For instance, some compilers implement functions such as isinf as macros in their header files.

If you use a cross compiler and create a Polyspace project from your build system, the project uses the header files provided by your compiler.