MATLAB: Convertion from U16 in U8 results overflow. Why

code proveroverflowpolyspacePolyspace Code ProverPolyspace Code Prover Serverr2014b

Hello all,
I made the following example:
    typedef unsigned int U16;
    typedef unsigned char U8;
    // case 1;     
    U16 a = 0x0FFF;
    U16 b = 0x0E00;
    U8 c = 0x00;
    //case 2:
    U16 d = 0xFFFF;
    U16 e = 0x0011;
    U16 f = 0;  
    void main()
    {  //case 1:
      c = (U8) (a-b); // -> red check overflow
      //case 2:
      f = (U8) ((d + e)&0x00FF); // + red warning -> no effect of 0x00FF
    }
When I run the Polyspace (Code Prover R2014b) analysis, I receive the following red checks:
1) Error: operation [conversion from unsigned int16 to unsigned int8] on scalar overflows (result is always strictly greater than MAX UINT8) conversion from unsigned int 16 to unsigned int 8
2) Error: operation [+] on scalar overflows (result is always strictly greater than MAX UINT16) operator + on type unsigned int 16
If I change the code from:
c = (U8) (a-b);
to
c = (U8) ((a-b)&0x00FF);
I don't receive the first red warning. Which is the correct configuration for overflow for no error occurring?

Best Answer

Hi,
I will also add that Polyspace is raising an overflow here because in your Polyspace project, you have specified an option to detect overflows on unsigned (see Check Behavior).
The C standard says that there is no overflow on unsigned types (a wrap-around is taking place if that happens), but Polyspace can be stricter than the ANSI C standard.
So if you want to get rid of this overflow on unsigned, you have to use the default mode for detecting overflow (signed only).
Best regards,
Alexandre
Related Question