CertC-INT33

Ensure that division and remainder operations do not result in divide-by-zero errors

Required inputs: IR, StaticSemanticAnalysis

The C Standard identifies the following condition under which division and remainder operations result in undefined behavior (UB):

UB Description
45 The value of the second operand of the  / or  % operator is zero (6.5.5).

Ensure that division and remainder operations do not result in divide-by-zero errors.

Division

The result of the / operator is the quotient from the division of the first arithmetic operand by the second arithmetic operand. Division operations are susceptible to divide-by-zero errors. Overflow can also occur during two's complement signed integer division when the dividend is equal to the minimum (most negative) value for the signed integer type and the divisor is equal to -1. (See INT32-C. Ensure that operations on signed integers do not result in overflow.)

Noncompliant Code Example

This noncompliant code example prevents signed integer overflow in compliance with INT32-C. Ensure that operations on signed integers do not result in overflow but fails to prevent a divide-by-zero error during the division of the signed operands  s_a and  s_b: 

#include <limits.h>
 
void func(signed long s_a, signed long s_b) {
  signed long result;
  if ((s_a == LONG_MIN) && (s_b == -1)) {
    /* Handle error */
  } else {
    result = s_a / s_b;
  }
  /* ... */
}
Compliant Solution

This compliant solution tests the division operation to guarantee there is no possibility of divide-by-zero errors or signed overflow:

#include <limits.h>
 
void func(signed long s_a, signed long s_b) {
  signed long result;
  if ((s_b == 0) || ((s_a == LONG_MIN) && (s_b == -1))) {
    /* Handle error */
  } else {
    result = s_a / s_b;
  }
  /* ... */
}
Remainder

The remainder operator provides the remainder when two operands of integer type are divided. 

Noncompliant Code Example

This noncompliant code example prevents signed integer overflow in compliance with INT32-C. Ensure that operations on signed integers do not result in overflow but fails to prevent a divide-by-zero error during the remainder operation on the signed operands  s_a and  s_b: 

#include <limits.h>
 
void func(signed long s_a, signed long s_b) {
  signed long result;
  if ((s_a == LONG_MIN) && (s_b == -1)) {
    /* Handle error */
  } else {
    result = s_a % s_b;
  }
  /* ... */
}
Compliant Solution

This compliant solution tests the remainder operand to guarantee there is no possibility of a divide-by-zero error or an overflow error:

#include <limits.h>
 
void func(signed long s_a, signed long s_b) {
  signed long result;
  if ((s_b == 0 ) || ((s_a == LONG_MIN) && (s_b == -1))) {
    /* Handle error */
  } else {
    result = s_a % s_b;
  }
  /* ... */
}
Risk Assessment

A divide-by-zero error can result in abnormal program termination and denial of service.

Rule Severity Likelihood Remediation Cost Priority Level
INT33-C Low Likely Medium P6 L2
Related Guidelines
Taxonomy Taxonomy item Relationship
CERT C INT32-C. Ensure that operations on signed integers do not result in overflow Prior to 2018-01-12: CERT: Unspecified Relationship
CERT Oracle Secure Coding Standard for Java NUM02-J. Ensure that division and remainder operations do not result in divide-by-zero errors Prior to 2018-01-12: CERT: Unspecified Relationship
ISO/IEC TS 17961 Integer division errors [diverr] Prior to 2018-01-12: CERT: Unspecified Relationship
CWE 2.11 CWE-369, Divide By Zero 2017-07-07: CERT: Exact
Bibliography
[ Seacord 2013b] Chapter 5, "Integer Security"
[ Warren 2002] Chapter 2, "Basics"
Excerpt from SEI CERT C Coding Standard: Rules for Developing Safe, Reliable, and Secure Systems (2016 Edition) and SEI CERT C Coding Standard [https://cmu-sei.github.io/secure-coding-standards/sei-cert-c-coding-standard/rules/integers-int/int33-c], Copyright (C) 1995-2026 Carnegie Mellon University. See section 9.4. "3rd-Party Licenses" in the documentation for full details.

Possible Messages

Key

Text

Severity

Disabled

division_by_zero

Division by zero

None

False

modulo_by_zero

Modulo by zero

None

False

possible_division_by_zero

Possible division by zero

None

False

possible_modulo_by_zero

Possible modulo by zero

None

False

Options

abstract_interpretation_div_by_zero

abstract_interpretation_div_by_zero : bool = True

Use additional "symbolic expression analysis" as postprocessing step. This can remove false positives, but might require more time. Option is automatically active if StaticSemanticAnalysis/performance.general.enhanced_analysis is active.
 

abstract_interpretation_maximal_tracked_array_index

abstract_interpretation_maximal_tracked_array_index : int = 10

The number of explicit indices in array expressions per routine tracked by the "symbolic expression analysis". For example, consider the following program. 

extern signed char a[6];
extern signed char x;
int main()
{
    if (a[2] < 0)
    {
        x = x / a[2];
    }
    if (a[3] < 0)
    {
        x = x / a[3];
    }
    if (a[4] < 0)
    {
        x = x / a[4];
    }
    return 0;
}

If the value of this option is set to 2, the first two array index expressions encountered in the routine are tracked. Hence, the analysis can use the facts a[2] < 0 and a[3] < 0 to infer that the respective divisions do not divide by zero, but it will not track the third array access in this routine.

A higher value of the option can cause more consumption of memory and time for the analysis.

 

abstract_interpretation_overflow_unrolling_level

abstract_interpretation_overflow_unrolling_level : int = 0

How many levels of conditions are traversed to compute additional constraints for the "symbolic expression analysis".