Main Content

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.

Note that even after extending the checkers, Bug Finder does not provide the sound and exhaustive analysis of Code Prover. For instance, if Bug Finder does not detect errors after extending the checkers, this absence of detected errors does not have the same guarantees as green checks in Code Prover.

Extend Checker

To extend the checker and detect the above issue, use these options:

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.

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:

Related Topics