Orange OBAI check in Polyspace Code Prover R2015a

3 views (last 30 days)
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]???

Answers (1)

Alexandre De Barros
Alexandre De Barros on 12 Dec 2017
Hi,
There is a similar question here:
You can also refer to the C standard, paragraph 6.5.2.1 "Array subscripting" (item 2) mentioning the type "integer".
Best regards,
Alex
  2 Comments
Dimo
Dimo on 13 Dec 2017
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
Alexandre De Barros on 19 Dec 2017
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

Sign in to comment.

Community Treasure Hunt

Find the treasures in MATLAB Central and discover how the community can help you!

Start Hunting!