Orange OBAI check in Polyspace Code Prover R2015a

4 次查看（过去 30 天）
Dimo
Dimo 2017-12-12
评论： Alexandre De Barros 2017-12-19
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]???

请先登录，再回答此问题。

回答（1 个）

Alexandre De Barros
Alexandre De Barros 2017-12-12
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
  2 个评论
Dimo
Dimo 2017-12-13
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 2017-12-19
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

请先登录，再进行评论。

类别

在 Help Center 和 File Exchange 中查找有关 Other Checks 的更多信息

标签

产品

Community Treasure Hunt

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

Start Hunting!

Translated by