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

Set the option using one of these methods:

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