Hello,
In standard C, there is no overflow on unsigned types. The C99 standard (§6.2.5/9) states:
"A computation involving unsigned operands can never overflow, because a result that cannot be represented by the resulting unsigned integer type is reduced modulo the number that is one greater than the largest value that can be represented by the resulting type."
Hence, by default, Code Prover will not report this kind of overflow.
Now, if you are interested by detecting them, you can change the default behavior thanks to the option "Detect overflows".
In the configuration pane, choose "Code Prover Verification" then "Check Behavior" and on the right page, for the option "Detect Overflows", select "signed and unsigned".
Please note that in your example, the overflow will appear on the assignment to the variable a, since the subtraction is performed on the int type (integral promotion).
Alex
