Hello,
I have noticed that Code Prover does not raise a warning in case of a subtraction between 2 unsigned variables. It does raise for 2 signed ones, but not with 2 unsigned.
Example
void test (void){ uint8_t a, b, c; b = foo(); c = bar(); a = b-c; }
This operation b-c is not seen as a potential overflow/underflow occurence.
Question
Is this an issue in CodeProver or a missing configuration, please?
Thank you for your answer,
Best regards
Best Answer