polyspace code prover: variable range does not change after function call

A simmilar code like the following I'm checking with polyspace codeprover 2014b.

...
  setAllToZero(myState);
  x = myState->myVariable;
...

In the function setAllToZero() the variable myState->myVariable is set to 0. But after the function Call polyspace asumes, that the variable has full range. Why is the range not [0]. Or what I'm doing wrong?

Thanks

best regards

Johannes

Answer 1

[Lucas Lebert]

Since this post is quite old I assume that the issue has already been resolved. Nevertheless I want to leave tips for users who encounter the same issue. The first thing I would check is, whether the struct the pointer is pointing to is a global variable and if it is assigned to a permanent range. To check this just hover over "myVariable" in the third line of the example above. If the range is specified as "permanent range" in the tooltip. The first step is to investigate the "Variable/function range setup" in the "Inputs & Stubbing" pane of the Configurations. For the struct change the Init mode from "Permanent" to for example "Init".

If the struct the pointer is pointing to is not a global variable then it is a whole other story and I would need to have a closer look at it.

Answer 2

[Jan Kablitz]

I have the same Problem! It seems that Polyspace does not mentioned the connection between the pointer and the corresponding variable.

[EDIT] I'am working with 2017b