Main Content

Round down results of negative integer division (-div-round-down)

Specify that your compiler rounds down a negative quotient from dividing two integers

Since R2023b

Description

The option with this name is available only in the Polyspace Platform (Polyspace Test) user interface. For the equivalent option in the standard Polyspace® user interface, see Division round down (-div-round-down).

Specify that your compiler rounds down a negative quotient from dividing two integers (such that it heads towards negative infinity). For instance, -5/3 rounds to -2. This option is equivalent to the Polyspace option Division round down (-div-round-down).

Set Option

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

Command line: 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

Version History

Introduced in R2023b

See Also

Topics