There is no way to make PolySpace accept dynamic arrays without modifying the source code that is being analyzed.
Please consider the following:
Replace this syntax
void foo(unsigned char a)
{
char b[a];
}
with this
void foo(unsigned char a)
{
#ifndef POLYSPACE
char b[a];
#else
char *b = (char *) malloc(sizeof(char) * a);
#endif
}
