Main Content

Division round down (-div-round-down)

Round down quotients from division or modulus of negative numbers instead of rounding up

Description

Specify whether quotients from division and modulus of negative numbers are rounded up or down.

Note

a = (a / b) * b + a % b is always true.

Set Option

User interface (desktop products only): In your project configuration, the option is on the Target & Compiler node.

User interface (Polyspace Platform, desktop products only): In your project configuration, the option is on the Build tab on the Target & Compiler node. This option is renamed to Round down results of negative integer division in the Polyspace® Platform user interface. See Round down results of negative integer division.

Command line and options file: Use the option -div-round-down. See Command-Line Information.

Why Use This Option

Use this option to emulate your compiler.

The option is relevant only for compilers following C90 standard (ISO/IEC 9899:1990). The standard stipulates that "if either operand of / or % is negative, whether the result of the / operator, is the largest integer less than or equal to the algebraic quotient or the smallest integer greater or equal than the quotient, is implementation defined, same for the sign of the % operator". The standard allows compilers to choose their own implementation.

For compilers following the C99 standard ((ISO/IEC 9899:1999), this option is not required. The standard enforces division with rounding towards zero (section 6.5.5).

Settings

On

If either operand of / or % is negative, the result of the / operator is the largest integer less than or equal to the algebraic quotient. The result of the % operator is deduced from a % b = a - (a / b) * b.  

Example: assert(-5/3 == -2 && -5%3 == 1); is true.

Off (default)

If either operand of / or % is negative, the result of the / operator is the smallest integer greater than or equal to the algebraic quotient. The result of the % operator is deduced from a % b = a - (a / b) * b.

This behavior is also known as rounding towards zero.

Example: assert(-5/3 == -1 && -5%3 == -2); is true.

Command-Line Information

Parameter: -div-round-down
Default: Off
Example (Bug Finder):  polyspace-bug-finder -div-round-down
Example (Code Prover): polyspace-code-prover -div-round-down
Example (Bug Finder Server): polyspace-bug-finder-server -div-round-down
Example (Code Prover Server): polyspace-code-prover-server -div-round-down

See Also

Topics