Orange OBAI check in Polyspace Code Prover R2015a

The code snippet below is verified with CodeProver R2015a. The tool detects an orange OBAI at line 11033 (iter [-2^31...2^31+1]). The variable iter is type unsigned int.

typedef uint8_least  Dcm_TimerIdType; 

typedef unsigned int uint8_least;   /* At least 8 bit                 */

Nevertheless at line 11033 the tool says array index value: [ -2^31...2^31+1]???

Answer 1

[Alexandre De Barros]

Hi,

There is a similar question here:

https://www.mathworks.com/matlabcentral/answers/101992-why-do-i-see-a-cast-to-signed-integer-on-my-unsigned-array-index

You can also refer to the C standard, paragraph 6.5.2.1 "Array subscripting" (item 2) mentioning the type "integer".

Best regards,

Alex

[Dimo]

Hi Alex,

Yes, it's true that the ANSI C standard says "integer" type for array index but this means both signed and unsigned integers (meaning any integer type like char(signed and unsigned), short(signed and unsigned), int(signed and unsigned), long(signed and unsigned), enum, bit-field) rather than just type int. I have read nowhere in the standard that array index will be converted to int. If this was true, then we would have negative array index in any situations like this:

//Assume 16-bit int

unsigned int i = 0xFFFE;//65534 decimal

int a[0xFFFF];
a[i] = 10; //after index conversion to int ----> a[-2]=10;

The only index conversion will occur only if the index is type char(signed or unsigned), short(signed or unsigned), enum or bit-field. The result type will be int if type int can represent all values of the original type, otherwise the result type will be unsigned int. This is part of so called integer promotions in C.

Regarding the relation between arrays and pointers:

a[i] is the same as *(a + i)

the standard explains the result from these operations but doesn't explain what kind of conversions occur on the operands.

At least this is my understanding on this topic.

[Alexandre De Barros]

Hello,

I have discussed with the development and this cast is indeed not "realistic". I have then created a request to discard this cast.

Regards,

Alex