Polyspace can view the initialized registers?

Hello all,

I started a new Polyspace Code Prover (R2014b) analysis for a project. In configuration, I checked “Ignore default initialization of global variables” from “Inputs & Stubbing” tab.

In Results Manager, I have 55 orange check with “non-initialized variable”. All of them are refering to sfrWords. I saw in Datasheets_uC that the sfrWords are writted by HW.

What should I do in this situation in order the Polyspace can view the initialized registers?

Thanks

[Rashmi Jadhav]

Hello,

I am also using Polyspace Code Prover (R2014b). Continuing with the query i want to know more details regarding the same topic "the Polyspace can view the initialized registers?" as:

If the file in which registers are initialized got disabled by some test and then we run the polyspace then will it be able to capture the initialization is missing? Or What will be the warning/Error from Polyspace occur to detect the initialization of that register?

Kindly reply.

Thanks in advance.

Answer 1

[Alexandre De Barros]

Hi Cristina,

I guess that the resigsters are declared as volatile, can you confirm ? Moreover, can you tell me how the registers are written in the code ?

Best regards,

Alexandre

Answer 2

[Cristina Golie]

Hello Alex,

Yes, the registers are declared as volatile.

You can see my attached file (register.txt).

Thanks you

Answer 3

[Cristina Golie]

here it is the attached file

[Alexandre De Barros]

Thanks.

Can you tell me if these registers are explicitely initialized in the code provided to Polyspace?

If not, then it is normal to have these orange "non-initialized variables" since the option "Ignore default initialization of global variables" is used to specify that Polyspace must not treat global variables as initialized. This is the goal of this option: being able to detect global variables which are not explicitely set to a value.

More information on this option of-global-variables-c.html here.

Now, if they are explicitely initialized somewhere in the code, can you show me an example of such initialization? Thanks.

Alex