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

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

Set the option using one of these methods:

• Polyspace Platform user interface (desktop products only): In your project configuration, on the Build tab, select the Target & Compiler node and then select this option.

• 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

Version History

Introduced in R2023b