Why Code Prover cannot detect Out of bound array index?

Global variable u1g_icsin_EmVari = [0.. 8]

=> This maybe a Out of bounds array index but Code Prover didn't show any warning related to this problem. why?

(There is a Green warning: Non initialized variable u1g_icsin_EmVari, but not any warning related to Out of bound array index)

Answer 1

[Anirban]

Hi Hong,

Please contact MathWorks Technical Support with a reproduction so that they can give you a specific diagnosis of the issue.

One possible explanation can be that this is a C++ project and the global array is "external" to the project. In other words, the file that defines the array (along with its size) has not been provided for the Polyspace analysis. For such "external" C++ arrays, since Code Prover does not know the size, by default, it does not show an Out of bounds array index (OBAI) check. You can use the option -consider-external-array-accesses-unsafe to see an orange OBAI check on this issue.

There can be many other reasons. Without some kind of a reproduction, it is difficult to tell.

PS. A more accurate answer is given in the last entry in this thread. Copying it here:

The Out of Bounds Array Index warning occurs when you read the memory location that is out of bounds (or possibly out of bounds). Just taking the address is not an issue per se.

[Tran Thang]

Thanks for answering.

I added that option in my options-file. But, Polyspace said that: "Option -consider-external-array-accesses-unsafe is unknown".

I try to change Cpp, also C-Cpp but this error still shows up.

[Anirban]

Which release of the product do you have?

[Tran Thang]

Polyspace R2019a

[Anirban]

This option is available from R2020a onwards. If this is indeed a C++ project, please contact MathWorks Technical Support for possible solutions for your release. First, a diagnosis needs to be made that indeed that the global array definition is not visible to the analysis. In a big project, many things could be happening. The reason does not seem to be clear from the code snippet itself.

[Tran Thang]

My project is C project and I updated to Polyspace R2020a but CodeProver still didn't show any OBAI check with the array above.

[Tran Thang]

Here is my CodeProver configuration. Is anything wrong?

[Anirban]

Hi Hong,

At this point, maybe Technical Support can help better. But let me try one more thing. I looked at the code more carefully and might have an idea. Sorry for not suggesting this earlier.

In your example, you are just taking the address of an array element. Can you try to dereference that address? You should get an Illegally Dereferenced Pointer warning. Alternatively, instead of taking the address, try reading the value directly. You should get an Out of Bounds Array Index warning.

The Out of Bounds Array Index warning occurs when you read the memory location that is out of bounds (or possibly out of bounds). Just taking the address is not an issue per se.

[Tran Thang]

Thank you very much.