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: