Review and Fix Division by Zero Checks

This topic describes how to systematically review the results of a Division by zero check in Polyspace^® Code Prover™.

Follow one or more of these steps until you determine a fix for the Division by zero check. There are multiple ways to fix a red or orange check. For a description of the check and code examples, see Division by zero.

Sometimes, especially for an orange check, you can determine that the check does not represent a real error but a Polyspace assumption that is not true for your code. If you can use an analysis option to relax the assumption, rerun the verification using that option. Otherwise, you can add a comment and justification in your result or code.

For the general workflow that applies to all checks, see Interpret Code Prover Results in Polyspace Desktop User Interface or Interpret Code Prover Results in Polyspace Access Web Interface (Polyspace Access).

Step 1: Interpret Check Information

Place your cursor on the / or % operation that causes the Division by zero error.

Obtain the following information from the tooltip:

• The values of the right operand (denominator).

  In the preceding example, the right operand, val, has a range that contains zero.

  Possible fix: To avoid the division by zero, perform the division only if val is not zero.

  Integer	Floating-point
  if(val != 0) func(1.0/val); else /* Error handling */	#define eps 0.0000001 . . if(val < -eps || val > eps) func(1.0/val); else /* Error handling */

• The probable root cause for division by zero, if indicated in the tooltip.

  In the preceding example, the software identifies a stubbed function, getVal, as probable cause.

  Possible fix: To avoid the division by zero, constrain the return value of getVal. For instance, specify that getVal returns values in a certain range, for example, 1..10. To specify constraints, use the analysis option Constraint setup (-data-range-specifications).

Step 2: Determine Root Cause of Check

Before a / or % operation, test if the denominator is zero. Provide appropriate error handling if the denominator is zero.

Only if you do not expect a zero denominator, determine root cause of check. Trace the data flow starting from the denominator variable. Identify a point where you can specify a constraint to prevent the zero value.

In the following example, trace the data flow starting from arg2:

void foo() {
	double time = readTime();
	double dist = readDist();
	.
	.
  bar(dist,time);
}

void bar(double arg1, double arg2) {
	double vel;
	vel=arg1/arg2;
}

You might find that:

1. bar is called with full-range of values.

   Possible fix: Call bar only if its second argument time is greater than zero.

2. time obtains a full-range of values from readTime.

   Possible fix: Constrain the return value of readTime, either in the body of readTime or through the Polyspace Constraint Specification interface, if you do not have the definition of readTime. For more information, see Code Prover Assumptions About Stubbed Functions.

To trace the data flow, select the check and note the information on the Result Details pane.

• If the Result Details pane shows the sequence of instructions that lead to the check, select each instruction.

• If the Result Details pane shows the line number of probable cause for the check, right-click the Source pane. Select Go To Line.

• Otherwise:

  1. Find the previous write operation on the operand variable.

     Example: The value of arg2 is written from the value of time in bar.

  2. At the previous write operation, identify a new variable to trace back.

     Place your cursor on the variables involved in the write operation to see their values. The values help you decide which variable to trace.

     Example: At bar(dist,time), you find that time has a full-range of values. Therefore, you trace time.

  3. Find the previous write operation on the new variable. Continue tracing back in this way until you identify a point to specify your constraint.

     Example: The previous write operation on time is time=readTime(). You can choose to specify your constraint on the return value of readTime.

Depending on the variable, use the following navigation shortcuts to find previous instances. You can perform the following steps in the Polyspace user interface only.

Variable	How to Find Previous Instances of Variable
Local Variable	Use one of the following methods: Search for the variable. Right-click the variable. Select Search For All References. All instances of the variable appear on the Search pane with the current instance highlighted. On the Search pane, select the previous instances. Browse the source code. Double-click the variable on the Source pane. All instances of the variable are highlighted. Scroll up to find the previous instances.
Global Variable Right-click the variable. If the option Show In Variable Access View appears, the variable is a global variable.	Select the option Show In Variable Access View. On the Variable Access pane, the current instance of the variable is shown. On this pane, select the previous instances of the variable. Write operations on the variable are indicated with and read operations with .
Function return value ret=func();	Find the function definition. Right-click func on the Source pane. Select Go To Definition, if the option exists. If the definition is not available to Polyspace, selecting the option takes you to the function declaration. In the definition of func, identify each return statement. The variable that the function returns is your new variable to trace back.

You can also determine if variables in any operation are related from some previous operation. See Find Relations Between Variables in Code.

Step 3: Look for Common Causes of Check

Look for common causes of the Division by zero check.

• For a variable that you expect to be non-zero, see if you test the variable in your code to exclude the zero value.

  Otherwise, Polyspace cannot determine that the variable has non-zero values. You can also specify constraints outside your code. See Specify External Constraints for Polyspace Analysis.

• If you test the variable to exclude its zero value, see if the test occurs in a reduced scope compared to the scope of the division.

  For example, a statement assert(var !=0) occurs in an if or while block, but a division by var occurs outside the block. If the code does not enter the if or while block, the assert does not execute. Therefore, outside the if or while block, Polyspace assumes that var can still be zero.

  Possible fix:

  • Investigate why the test occurs in a reduced scope. In the above example, see if you can place the statement assert(var !=0) outside the if or for block.

  • If you expect the if or while block to always execute, investigate when it does not execute.

Step 4: Trace Check to Polyspace Assumption

See if you can trace the orange check to a Polyspace assumption that occurs earlier in the code. If the assumption does not hold true in your case, add a comment or justification in your result or code. See Address Results in Polyspace User Interface Through Bug Fixes or Justifications or Address Results in Polyspace Access Through Bug Fixes or Justifications (Polyspace Access).

For instance, you are using a volatile variable in your code. Then:

1. Polyspace assumes that the variable is full-range at every step in the code. The range includes zero.

2. A division by the variable can cause Division by zero error.

3. If you know that the variable takes a non-zero value, add a comment and justification describing why you did not change your code.

For more information, see Code Prover Analysis Assumptions.

Note

Before justifying an orange check, consider carefully whether you can improve your coding design.

Disabling This Check

You can effectively disable this check. If your compiler supports infinities and NaNs from floating-point operations, you can enable a verification mode that incorporates infinities and NaNs. See Consider non finite floats (-allow-non-finite-floats).