DRS option is limited in Polyspace Code Prover

Hi guys,

I have this C++ code below:

void myfunc(int *arg, char *argv[])

{

if (*arg == 1)

*arg += 1;

char *p = argv[*arg];

if (p[0] == '-')

*arg += 1;

}

One of the Polyspace result is: Pointer may be outside its bounds. If appropriate, applying DRS to arg (argument number 1 of function myfunc(int *, char **), may remove this orange.

But when I tried to add and configure DRS, it has limited option as shown below:

There are no other options. Init Mode, Init Range and Initialize Pointer are disabled in this case.

Thank you in advance.

Answer 1

[Anirban]

In C++, you cannot constrain pointer arguments of functions using this interface. See Constraint Specification Limitations. The message about DRS in the results is applicable to C code only.

To work around this limitation, you can write manual main()-s of the kind documented here. But depending on the kind of constraint you want to specify, it might be difficult to write an appropriate main(). If you contact MathWorks Technical Support and tell them what kind of constraint you want to specify, they might be able to help you setup this main() .

[Zulham Mr]

Thank you for your explanation.