Skip to content

[Guideline] Add do not divide by 0 #132

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

[Guideline] Add do not divide by 0 #132

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 40 additions & 0 deletions src/coding-guidelines/expressions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,3 +81,43 @@ Expressions
}

fn with_base(_: &Base) { ... }

.. guideline:: Do not divide by 0
:id: gui_kMbiWbn8Z6g5
:category: Mandatory
:status: draft
:release: latest
:fls: fls_Q9dhNiICGIfr
:decidability: Undecidable
Copy link

@felix91gr felix91gr Jun 11, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Whether the program is or isn't dividing by zero is indeed Undecidable.

But whether the program is performing checked arithmetic or not is Decidable. So... perhaps this guideline should be changed to enforce checked arithmetic?

By which I mean: maybe it shouldn't be "Do not divide by 0". Maybe it should always be checked arithmetic.

Let's talk about it on Zulip!

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Whether the program is or isn't dividing by zero is indeed Undecidable.

Hmm. Does that make this quite onerous to the engineer which must comply with this?

Perhaps it could be advisory to allow easy deviation.

Maybe it should always be checked arithmetic.

This might be the right choice for another guideline, perhaps required which would make every division use checked_div().

What do you think @vapdrs?

:scope: System
:tags: numerics

This guideline applies when unsigned integer or two’s complement division is performed. This includes the
evaluation of a remainder expression.

.. rationale::
:id: rat_h84NjY2tLSBW
:status: draft

Integer division by zero results in a panic, which is an abnormal program state and may terminate the process.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed. It's even worse than that. Division by zero is Undefined Behavior, which is instant death for Safety Critical purposes :3

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point -- let's call that out here @vapdrs.


.. non_compliant_example::
:id: non_compl_ex_LLs3vY8aGz0F
:status: draft

When the division is performed, the right operand is evaluated to zero and the program panics.

.. code-block:: rust

let x = 0;
let x = 5 / x;

.. compliant_example::
:id: compl_ex_Ri9pP5Ch3kbb
:status: draft

There is no compliant way to perform integer division by zero
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should we leave the example code blank then?


.. code-block:: rust

let x = 5 % 5;