Orange OBAI check in Polyspace Code Prover R2015a

5 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
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!