FaultDetection-DivisionByZero

Avoid division by zero

Required inputs: IR, StaticSemanticAnalysis

This check detects divisions and modulo operations where the divisor could be zero (causing a runtime error).

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

• This rule shares the following common options: exclude_in_macros, exclude_messages_in_system_headers, excludes, extend_exclude_to_macro_invocations, includes, justification_checker, languages, post_processing, provider, report_at, severity

• The following places define options that affect this rule: Stylechecks, Analysis-GlobalOptions

abstract_interpretation_div_by_zero

abstract_interpretation_div_by_zero : bool = False

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".