Main Content

Differences Between Polyspace Bug Finder and Polyspace Code Prover

Polyspace® Bug Finder™ and Polyspace Code Prover™ detect run-time errors through static analysis. Though the products have a similar user interface and the mathematics underlying the analysis can sometimes be the same, the goals of the two products are different.

Bug Finder (or Polyspace as You Code, which performs a single-file analysis similar to Bug Finder) quickly analyzes your code and detects many types of defects. Code Prover checks every operation in your code for a set of possible run-time errors and tries to prove the absence of the error for all execution paths.

Note

For each operation in your code, Code Prover considers all execution paths leading to the operation that do not have a previous error. If an execution path contains an error prior to the operation, Code Prover does not consider it. See Code Prover Analysis Following Red and Orange Checks.

For instance, for every division in your code, a Code Prover analysis tries to prove that the denominator cannot be zero. Bug Finder does not perform such exhaustive verification. For instance, Bug Finder also checks for a division by zero error, but it might not find all operations that can cause the error.

The two products involve differences in setup, analysis and results review, because of this difference in objectives. In the following sections, we highlight the primary differences between a Bug Finder and a Code Prover analysis (also known as verification). Depending on your requirements, you can incorporate one or both kinds of analyses at appropriate points in your software development life cycle.

Overview of Differences Between Bug Finder and Code Prover

Use both Bug Finder and Code Prover regularly in your development process. The products provide a unique set of capabilities and complement each other. For possible ways to use the products together, see Workflow Using Both Polyspace Bug Finder and Polyspace Code Prover.

This table provides an overview of how the products complement each other. For details, see the sections below.

FeatureBug FinderCode Prover
Number of checkers300+ checkers for defects30 checks for critical run-time errors and 4 checks on global variable usage
Depth of analysis

Fast.

For instance:

  • Faster analysis.

  • Easier set up and review.

  • Fewer runs for clean code.

  • Results in real time.

Exhaustive.

For instance:

  • All operations of a type checked for certain critical errors.

  • More rigorous data and control flow analysis.

Reporting criteriaProbable defectsProven findings
Bug finding criteriaFew false positivesZero false negatives

How Bug Finder and Code Prover Complement Each Other

Faster Analysis with Bug Finder

How much faster the Bug Finder analysis is depends on the size of the application. The Bug Finder analysis time increases linearly with the size of the application. The Code Prover verification time increases at a rate faster than linear.

One possible workflow is to run Code Prover to analyze modules or libraries for robustness against certain errors and run Bug Finder at integration stage. Bug Finder analysis on large code bases can be completed in a much shorter time, and also find integration defects such as Declaration mismatch and Data race.

More Exhaustive Verification with Code Prover

Code Prover tries to prove the absence of:

  • Division by Zero error on every division or modulus operation

  • Out of Bounds Array Index error on every array access

  • Non-initialized Variable error on every variable read

  • Overflow error on every operation that can overflow

and so on.

For each operation:

  • If Code Prover can prove the absence of the error for all execution paths, it highlights the operation in green.

  • If Code Prover can prove the presence of a definite error for all execution paths, it highlights the operation in red.

  • If Code Prover cannot prove the absence of an error or presence of a definite error, it highlights the operation in orange. This small percentage of orange checks indicate operations that you must review carefully, through visual inspection or testing. The orange checks often indicate hidden vulnerabilities. For instance, the operation might be safe in the current context but fail when reused in another context.

    You can use information provided in the Polyspace user interface to diagnose the checks. See More Rigorous Data and Control Flow Analysis with Code Prover. You can also provide contextual information to reduce unproven code even further, for instance, constrain input ranges externally.

Bug Finder does not aim for exhaustive analysis. It tries to detect as many bugs as possible and reduce false positives. For critical software components, running a bug finding tool is not sufficient because despite fixing all defects found in the analysis, you can still have errors during code execution (false negatives). After running Code Prover on your code and addressing the issues found, you can expect the quality of your code to be much higher. See Zero False Negatives with Code Prover.

More Specific Defect Types with Bug Finder

Code Prover checks for types of run-time errors where it is possible to mathematically prove the absence of the error. In addition to detecting errors whose absence can be mathematically proven, Bug Finder also detects other defects.

For instance, the statement if(a=b) is semantically correct according to the C language standard, but often indicates an unintended assignment. Bug Finder detects such unintended operations. Although Code Prover does not detect such unintended operations, it can detect if an unintended operation causes other run-time errors.

Examples of defects detected by Bug Finder but not by Code Prover include good practice defects, resource management defects, some programming defects, security defects, and defects in C++ object oriented design.

For more information, see:

  • Defects: List of defects that Bug Finder can detect.

  • Run-Time Checks: List of run-time errors that Code Prover can detect.

Easier Setup Process with Bug Finder

Even if your code builds successfully in your compilation toolchain, it can fail in the compilation phase of a Code Prover verification. The strict compilation in Code Prover is related to its ability to prove the absence of certain run-time errors.

  • Code Prover strictly follows the ANSI® C99 Standard, unless you explicitly use analysis options that emulate your compiler.

    To allow deviations from the ANSI C99 Standard, you must use the Target and Compiler options. If you create a Polyspace project from your build system, the options are automatically set.

  • Code Prover does not allow linking errors that common compilers can permit.

    Though your compiler permits linking errors such as mismatch in function signature between compilation units, to avoid unexpected behavior at run time, you must fix the errors.

For more information, see Troubleshoot Compilation and Linking Errors.

Bug Finder is less strict about certain compilation errors. Linking errors, such as mismatch in function signature between different compilation units, can stop a Code Prover verification but not a Bug Finder analysis. Therefore, you can run a Bug Finder analysis with less setup effort. In Bug Finder, linking errors are often reported as a defect after the analysis is complete.

Fewer Runs for Clean Code with Bug Finder

To guarantee absence of certain run-time errors, Code Prover follows strict rules once it detects a run-time error in an operation. Once a run-time error occurs, the state of your program is ill-defined and Code Prover cannot prove the absence of errors in subsequent code. Therefore:

  • If Code Prover proves a definite error and displays a red check, it does not verify the remaining code in the same block.

    Exceptions include checks such as Overflow, where the analysis continues with the result of overflow either truncated or wrapped around.

  • If Code Prover suspects the presence of an error and displays an orange check, it eliminates the path containing the error from consideration. For instance, if Code Prover detects a Division by Zero error in the operation 1/x, in the subsequent operation on x in that block, x cannot be zero.

  • If Code Prover detects that a code block is unreachable and displays a gray check, it does not detect errors in that block.

For more information, see Code Prover Analysis Following Red and Orange Checks.

Therefore, once you fix red and gray checks and rerun verification, you can find more issues. You need to run verification several times and fix issues each time for completely clean code. The situation is similar to dynamic testing. In dynamic testing, once you fix a failure at a certain point in the code, you can uncover a new failure in subsequent code.

Bug Finder does not stop the entire analysis in a block after it finds a defect in that block. Even with Bug Finder, you might have to run analysis several times to obtain completely clean code. However, the number of runs required is fewer than Code Prover.

Results in Real Time with Bug Finder

Bug Finder shows some analysis results while the analysis is still running. You do not have to wait until the end of the analysis to review the results.

Code Prover shows results only after the end of the verification. Once Bug Finder finds a defect, it can display the defect. Code Prover has to prove the absence of errors on all execution paths. Therefore, it cannot display results during analysis.

More Rigorous Data and Control Flow Analysis with Code Prover

For each operation in your code, Code Prover provides:

  • Tooltips showing the range of values of each variable in the operation.

    For a pointer, the tooltips show the variable that the pointer points to, along with the variable values.

  • Graphical representation of the function call sequence that leads to the operation.

By using this range information and call graph, you can easily navigate the function call hierarchy and understand how a variable acquires values that lead to an error. For instance, for an Out of Bounds Array Index error, you can find where the index variable is first assigned values that lead to the error.

When reviewing a result in Bug Finder, you also have supporting information to understand the root cause of a defect. For instance, you have a traceback from where Bug Finder found a defect to its root cause. However, in Code Prover, you have more complete information, because the information helps you understand all execution paths in your code.

Data Flow Analysis in Code Prover

Control Flow Analysis in Code Prover

Few False Positives with Bug Finder

Bug Finder aims for few false positives, that is, results that you are not likely to fix. By default, you are shown only the defects that are likely to be most meaningful for you.

Bug Finder also assigns an attribute called impact to the defect types based on the criticality of the defect and the rate of false positives. You can choose to analyze your code only for high-impact defects. You can also enable or disable a defect that you do not want to review.

You can also disable certain Code Prover defects related to non-initialization.

Zero False Negatives with Code Prover

Code Prover aims for an exhaustive analysis. The software checks every operation that can trigger specific types of error. If a code operation is green, it means that the operation cannot cause those run-time errors that the software checked for. In this way, the software aims for zero false negatives.

The Code Prover result holds only if you execute your code under the same conditions that you supplied to Code Prover through the analysis options.

If the software cannot prove the absence of an error, it highlights the suspect operation in red or orange and requires you to review the operation.

Coding Rule Support in Bug Finder

Bug Finder supports checking for compliance with external coding standards, such as:

For the complete list of coding standards support, see Polyspace Support for Coding Standards.

Related Topics