Review and Fix User Assertion Checks

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

Follow one or more of these steps until you determine a fix for the User assertion check. There are multiple ways to fix this check. For a description of the check and code examples, see User assertion.

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).

How to use this check: Typically you use assert statements during debugging to check if a condition is satisfied at the current point in your code. For instance, if you expect a variable var to have values in a range [1,10] at a certain point in your code, you place the following statement at that point:

assert(var >=1 && var <= 10);

Polyspace statically determines whether the condition is satisfied.

Therefore, you can judiciously insert assert statements that test for requirements from your code.

• A red result for the User assertion check indicates that the requirement is definitely not met.

• An orange result for the User assertion check indicates that the requirement is possibly not met.

Step 1: Determine Root Cause of Check

Trace the data flow for each variable involved in the assert statement.

In the following example, trace the data flow for myArray.

int* getArray(int numberOfElements) {
    .
    .
    arrayPtr = (int*) malloc(numberOfElements);
    .
    .
    return arrayPtr;
}
void func() {
    int* myArray = getArray(10);
    assert(myArray!=NULL);
    .
    .
}

In this example, it is possible that in getArray, the return value of malloc is not checked for NULL.

Possible fix: If you expect a certain requirement, see if you have tests that enforce the requirement. In this example, if you expect getArray to return a non-NULL value, in getArray, test the return value of malloc for NULL.

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 in the Source pane. Select Go To Line. Enter the line number.

• Otherwise, for each variable involved in the condition, find previous instances and trace back to the root cause of the check. For more information on common root causes, see Step 3: Look for Common Causes of Check.

  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 2: Look for Common Causes of Check

1. If the check is orange and occurs in a function, see if the function is called multiple times. Determine if the assertion fails only on certain calls. For those calls, navigate to the caller body and see if you have tests that enforce your assertion requirement.

   • To see the callers of a function, select the function name on the Source pane. All callers appear on the Call Hierarchy pane. Select a caller name to navigate to it in your source.

   • To determine if a subset of calls cause the orange check, use the option Sensitivity context (-context-sensitivity). For a tutorial, see Identify Function Call with Run-Time Error.

2. If you have tests that enforce the assertion requirement, see if:

   • The assertion statement is within the scope of the tests.

   • You modify the test variables between the test and the assertion.

   For instance, the test if(index < SIZE) enforces that index is less than SIZE. However, the assertion assert(index < SIZE) can fail if:

   • It occurs outside the if block.

   • Before the assertion, you modify index in the if block.

   Possible fix: Consider carefully whether you must meet your assertion requirements. If you must meet those requirements, place tests that enforce your requirement. After the tests, avoid modifying the test variables.

Step 3: 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, after a function call, you assert a relation between two variables. Then:

1. Depending on the depth of the function call and the complexity of your code, Polyspace can sometimes approximate the variable ranges. Because of the approximation, the software cannot establish if the relation holds and produces an orange User assertion check.

2. Run dynamic tests on the orange check to determine if the assertion fails.

3. Try to reduce your code complexity and rerun the verification. Otherwise, add a comment and a justification in your result or code 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.