Issue

Polyspace^® uses its own implementation of standard library functions for more efficient analysis. If you redefine a standard library function and provide the function body to Polyspace, the analysis uses your definition.

However, for certain standard library functions, Polyspace continues to use its own implementations, even if you redefine the function and provide the function body. The functions include assert and memory allocation functions such as malloc, calloc and alloca.

You see a warning message like the following:

Body of routine "malloc" was discarded.

Cause

These functions have special meaning for the Polyspace analysis, so you are not allowed to redefine them. For instance:

Solution

Unless you particularly want your own redefinitions to be used, ignore the warning. The analysis results are based on Polyspace implementations of the standard library function, which follow the original function specifications.

If you want your own redefinitions to be used and you are sure that your redefined function behaves the same as the original function, rename the functions. You can rename the function only for the purposes of analysis using the option Preprocessor definitions (-D). For instance, to rename a function malloc to my_malloc, use malloc=my_malloc for the option argument.