Dynamic arrays are a feature of the C99 standard (called also variable-length arrays) and they cannot be actually used with PolySpace Client for C/C++ (C language).
As a workaround, replace the declaration of the array by a declaration containing a call to malloc. For example:
void foo(unsigned char a)
{
char b[a];
}
can be replaced by :
#include <stdlib>
void foo(unsigned char a)
{
#ifndef POLYSPACE
char b[a];
#else
char *b = (char *) malloc(sizeof(char) * a);
#endif
}
The goal of the #ifndef directive is to keep the original code when the C file is used with a compiler, and to use the malloc when the C file is analyzed with PolySpace.
Note: the compilation flag POLYSPACE should be added to the list of flags (-D option).
Best Answer