Orange OBAI check in Polyspace Code Prover R2015a

5 visualizzazioni (ultimi 30 giorni)
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]???

Risposte (1)

Alexandre De Barros
Alexandre De Barros il 12 Dic 2017
There is a similar question here:
You can also refer to the C standard, paragraph "Array subscripting" (item 2) mentioning the type "integer".
Best regards,
  2 Commenti
Alexandre De Barros
Alexandre De Barros il 19 Dic 2017
I have discussed with the development and this cast is indeed not "realistic". I have then created a request to discard this cast.

Accedi per commentare.

Community Treasure Hunt

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

Start Hunting!

Translated by