Do not divide by 0

Guideline: Do not divide by 0 gui_kMbiWbn8Z6g5

status: draft

tags: numerics, defect

category: required

fls: fls_Q9dhNiICGIfr

decidability: undecidable

scope: system

release: latest

child needs: rat_h84NjY2tLSBW, non_compl_ex_LLs3vY8aGz0F, compl_ex_Ri9pP5Ch3kcc, bib_kMbiWbn8Z6g5

Integer division by zero results in a panic. This includes both division expressions [FLS-DIVISION-EXPR] and remainder expressions [FLS-REMAINDER-EXPR].

Division and remainder expressions on signed integers are also susceptible to arithmetic overflow. Overflow is covered in full by the guideline Ensure that integer operations do not result in arithmetic overflow.

This rule applies to the following primitive integer types [FLS-INTEGER-TYPES]:

i8

i16

i32

i64

i128

u8

u16

u32

u64

u128

usize

isize

This rule does not apply to evaluation of the core::ops::Div trait on types other than integer types [FLS-INTEGER-TYPES].

This rule is a less strict version of Do not use an integer type as a divisor during integer division. All code that complies with that rule also complies with this rule.

Rationale: rat_h84NjY2tLSBW

status: draft

parent needs: gui_kMbiWbn8Z6g5

Integer division by zero results in a panic; an abnormal program state that may terminate the process and must be avoided.

Non-Compliant Example: non_compl_ex_LLs3vY8aGz0F

status: draft

parent needs: gui_kMbiWbn8Z6g5

This non-compliant example panics when the right operand is zero for either the division or remainder operations.

compile fail

fn main() {
    let x = 0;
    let _y = 5 / x; // Results in a panic.
    let _z = 5 % x; // Also results in a panic.
}

Compliant Example: compl_ex_Ri9pP5Ch3kcc

status: draft

parent needs: gui_kMbiWbn8Z6g5

Compliant examples from Do not use an integer type as a divisor during integer division are also valid for this rule. Additionally, the check for zero can be performed manually, as in this compliant example. However, as the complexity of the control flow leading to the invariant increases, it becomes increasingly harder for both programmers and static analysis tools to reason about it.

Note that the test for arithmetic overflow is not necessary for unsigned integers.

fn main() {
    // Checking for zero by hand
    let x = 0u32;
    let _y = if x != 0u32 {
        5u32 / x
    } else {
        0u32
    };

    let _z = if x != 0u32 {
        5u32 % x
    } else {
        0u32
    };
}

Bibliography: bib_kMbiWbn8Z6g5

status: draft

parent needs: gui_kMbiWbn8Z6g5

[FLS-INTEGER-TYPES]↩	The Rust FLS. “Types and Traits - Integer Types.” https://rust-lang.github.io/fls/types-and-traits.html#integer-types
[FLS-DIVISION-EXPR]↩	The Rust FLS. “Expressions - Syntax - DivisionExpression.” https://rust-lang.github.io/fls/expressions.html#syntax_divisionexpression
[FLS-REMAINDER-EXPR]↩	The Rust FLS. “Expressions - Syntax - RemainderExpression.” https://rust-lang.github.io/fls/expressions.html#syntax_remainderexpression