How to fix Polyspace CodeProver Orange warnings due to + operator

Hello,

I am getting a Polyspace CodeProver Orange Overflow error due to + operator in the attached code

How to fix these issues as we are sure the expression is not going to generate a result that can extend beyond the data type of int32 ?

Answer 1

[Arnav]

Hi @Dinesh Kumar,

Assuming that the result of the sum will not overflow. You can bypass the Code Prover warning by asserting the operands to lie in a plausible range. For example, this can be done as shown below:

        int number1=9, number2=9;
        scanf("%d %d",&number1, &number2);
        #ifdef POLYSPACE
        unchecked_assert(number1 < 10 && number1 > -10);
        unchecked_assert(number2 < 10 && number2 > -10);
        #endif
        int result = number1 + number2; //Source of Warning

unchecked_assert is used instead of assert due to additional orange warnings being generated due to possibility of failing assert statements. Polyspace Code Prover does not check unchecked_assert statements.

The unchecked_assert statements are placed inside an include guard. Before running the Code Prover analysis, you need to include the guard preprocessor macro as shown:

It should be noted that any suppression of warnings should be well-documented and justified to maintain code safety and readability.

• You may look at other ways to specify constraints in Polyspace here:

https://www.mathworks.com/help/releases/R2020b/polyspace_code_prover_server/ug/drs-configuration-settings.html

• You can refer to the below MATLAB Answers thread for more information:

https://www.mathworks.com/matlabcentral/answers/1746135-polyspace-overflow-orange-checks