Main Content

Overflow

Arithmetic operation causes overflow

expand all in page

Description

This check on an arithmetic operation determines whether the result overflows. The result of this check depends on whether you allow nonfinite float results such as infinity and NaN.

The result of the check also depends on the float rounding mode you specify. By default, the rounding mode is to-nearest. See Float rounding mode (-float-rounding-mode).

Nonfinite Floats Not Allowed

By default, nonfinite floats are not allowed. When the result of an operation falls outside the allowed range, an overflow occurs. The check is:

  • Red, if the result of the operation falls outside the allowed range.

  • Orange, if the result of the operation falls outside the allowed range on some of the execution paths.

  • Green, if the result of the operation does not fall outside the allowed range.

To fine tune the behavior of the overflow check, use these options and specify argument forbid, allow, or warn-with-wrap-around:

The operand data types determine the allowed range for the arithmetic operation. If the operation involves two operands, the verification uses the ANSI® C conversion rules to determine a common data type. This common data type determines the allowed range.

For some examples of conversion rules, see Code Prover Assumptions About Implicit Data Type Conversions.

Nonfinite Floats Allowed

If you enable a verification mode that incorporates infinities and specify that the verification must warn about operations that produce infinities, the check is:

  • Red, if the operation produces infinity on all execution paths that the software considers, and the operands themselves are not infinite.

  • Orange, if the operation produces infinity on some of the execution paths when the operands themselves are not infinite.

  • Green, if the operation does not produce infinity unless the operands themselves are infinite.

If you specify that the verification must forbid operations that produce infinities, the check color depends on the result of the operation only. The color does not depend on the operands.

To enable this verification mode, use these options:

Diagnosing This Check

Review and Fix Overflow Checks

Examples

expand all

void main() {
  int i=1;
  i = i << 30; //i = 2^30
  i = 2*i-2;
}

In this example, the operation 2*i results in a value 231. The Overflow check on the multiplication produces a red error because the maximum value that the type int can hold on a 32–bit target is 231-1.

void main(void)
 {
   int i;
   int shiftAmount = 1;

   i = 1090654225 << shiftAmount; 
 }

In this example, an Overflow error occurs a left shift is performed on a signed integer.

#include <float.h>

void main() {
 float val = FLT_MAX;
 val = val * 2 + 1.0;
}

In this example, FLT_MAX is the maximum value that float can represent on a 32-bit target. Therefore, the operation val * 2 results in an Overflow error.

void func(void) {
   float fVal = -2.0f;
   unsigned int iVal = (unsigned int)fVal; 
}

In this example, a red Overflow check appears on the cast from float to unsigned int. According to the C99 Standard (footnote to paragraph 6.3.1.4), the range of values that can be converted from floating-point values to unsigned integers while keeping the code portable is (-1, MAX + 1). For floating-point values outside this range, the conversion to unsigned integers is not well-defined. Here, MAX is the maximum number that can be stored by the unsigned integer type.

Even if a run-time error does not occur when you execute the code on your target, the cast might fail on another target.

Correction — Cast to Signed Integer First

One possible solution is to cast the floating-point value to a signed integer first. The signed integer can then be cast to an unsigned integer type. For these casts, the conversion rules are well-defined.

void func(void) {
   float fVal = -2.0f;
   int iValTemp = (int)fVal;
   unsigned int iVal = (unsigned int)iValTemp; 
}
#define FLT_MAX 3.40282347e+38F

void float_negative_overflow() {
   float min_float = -FLT_MAX;
   min_float = -min_float * min_float;
}

In float_negative_overflow, min_float contains the most negative number that the type float can represent. Because the operation -min_float * min_float produces a number that is more negative than this number, the type float cannot represent it. The Overflow check produces a red error.

#include <stdio.h>

struct
{
  unsigned int dayOfWeek : 2;
} Week;

void main()
{
  unsigned int two = 2, three = 3, four = 4;
  Week.dayOfWeek = two;
  Week.dayOfWeek = three;
  Week.dayOfWeek = four;
}

In this example, dayOfWeek occupies 2 bits. It can take values in [0,3] because it is an unsigned integer. When you assign the value 4 to dayOfWeek, the Overflow check is red.

To detect overflows on signed and unsigned integers, on the Configuration pane, under Check Behavior, select forbid or warn-with-wrap-around for Overflow mode for signed integer and Overflow mode for unsigned integer.

Results in forbid mode:

double func(void) {
    double x=1.0/0.0;
    return x;
}
In this example, both the operands of the / operation is not infinite but the result is infinity. The Overflow check on the - operation is red. In the forbid mode, the verification stops after the red check. For instance, a Non-initialized local variable check does not appear on x in the return statement. If you do not turn on the option Allow non finite floats, a Division by zero check appears because infinities are not allowed.

Results in warn-first mode:

double func(void) {
    double x=1.0/0.0;
    return x;
}
In this example, both the operands of the / operation are not infinite but the result is infinity. The Overflow check on the - operation is red. The red checks in warn-first mode are different from red checks for other check types. The verification does not stop after the red check. For instance, a green Non-initialized local variable check appears on x in the return statement. In the verification result, if you place your cursor on x, you see that it has the value Inf.

Results in forbid mode:

void func(double arg1, double arg2) {
    double ratio1=arg1/arg2;
    double ratio2=arg1/arg2;
}
In this example, the values of arg1 and arg2 are unknown to the verification. The verification assumes that arg1 and arg2 can have all possible double values. For instance, arg1 can be nonzero and arg2 can be zero and the result of ratio1=arg1/arg2 can be infinity. Therefore, an orange Overflow check appears on the division operation. Following the check, the verification terminates the execution thread that results in infinity. The verification assumes that arg2 cannot be zero following the orange check. The Overflow check on the second division operation ratio2=arg1/arg2 is green.

Results in warn-first mode:

void func(double arg1, double arg2) {
    double ratio1=arg1/arg2;
    double ratio2=arg1/arg2;
}
In this example, the values of arg1 and arg2 are unknown to the verification. The verification assumes that arg1 and arg2 can have all possible double values. For instance, arg1 can be non-zero and arg2 can be zero and the result of ratio1=arg1/arg2 can be infinity. An orange Overflow check appears on the division operation. The orange checks in warn-first mode are different from orange checks for other check types. Following the check, the verification does not terminate the execution thread that results in infinity. The verification retains the zero value of arg2 following the orange check. Therefore, the Overflow check on the second division operation ratio2=arg1/arg2 is also orange.

Check Information

Group: Numerical
Language: C | C++
Acronym: OVFL

See Also

| | | | | |

Topics