MISRA C 2012: 13.2 rule warning on Polyspace Code Prover R2014b

I made the following example from "MISRA C 2012" pdf file:

*extern volatile int PORT;

void main() {

PORT = PORT & 0x80;

}*

When I run the Polyspace (Code Prover R2014b) analysis, I receive the following Misra C:2012 13.2 warning:

"The value of an expression and its persistent side effects shall be the same under all permitted evaluation orders. The value of volatile 'PORT' depends on the order of evaluation because of multiple accesses. (Required)"

In "MISRA C 2012" pdf file, is mentioned that the above example is a compliant one.

Is this a MISRA C document type error?

Answer 1

[Alexandre De Barros]

Hello Cristina,

The MISRA C 2012 document is correct. The version R2015b of the Polyspace products will not give you this warning.

Best regards,

Alex