Extend Bug Finder Checkers to Find Defects from Specific System Input Values

This topic shows how to find possible defects from specific values of system inputs. Unlike Code Prover, Bug Finder does not exhaustively check for run-time errors for all combinations of system inputs. However, you can extend some Bug Finder checkers and find if there are specific system input values that can lead to run-time errors.

Identify Need for Extending Checker

First identify if an existing checker is sufficient for your requirements.

For instance, the Bug Finder checker Integer division by zero detects if a division operation can have a zero denominator. Suppose, a library function has the possibility of a division by zero following several numerical operations. For instance, consider the function speed here:

#include <assert.h>

int speed(int k) {
    int i,j,v;
    i=2;
    j=k+5;
    while (i <10) {
            i++;
            j+=3;
    }

    v = 1 / (i-j); 
    return v+k;
}
Suppose you see a sporadic run-time error when your program execution enters this function and the default Bug Finder analysis does not detect the issue. To minimize false positives, the default analysis might suppress issues from specific values of an unknown input (what if this value did not occur in practice at run time?). See also Inputs in Polyspace Bug Finder. To find the root cause of the sporadic error, you can run a stricter Bug Finder analysis for just this function.

Bug Finder does not provide the sound and exhaustive analysis of Code Prover. For sound and exhaustive analysis, run a Polyspace® Code Prover™ analysis instead of extending Bug Finder checkers.

Extend Checker

To extend the checker and detect the above issue, use the option Run stricter checks considering all values of system inputs (-checks-using-system-input-values). With this option, checkers that rely on numerical values considers all input values for functions with at least one callee. You can change which functions are considered by using the option Consider inputs to these functions (-system-inputs-from). For this option, use the value custom and enter the name of the function whose inputs must be considered.

For example, to consider the inputs of the function speed in the preceding code, use the option argument custom=speed

When you run a Bug Finder analysis, you see a possible integer division by zero on the division operation. The result shows an example of an input value to the function speed that eventually leads to the current defect (zero value of the denominator).

The tooltips on the defect show how the input value propagates through the code to eventually lead to one set of values that cause the defect. For example, the tooltip on the line int speed(int k) shows that an input value of -19 results in the defect Integer division by zero.

Tooltips on variables in source code show how the input value of -19 leads to the final values that cause the division by zero defect.

Checkers That Can Be Extended

The following checkers are affected by numerical values of inputs and can be extended using the preceding options:

See Also

Topics