-classification

Control precisely which files to include in Polyspace analysis and how to analyze them

Since R2023a

Syntax

-classification <file>

Description

-classification <file> specifies which files to include in a Polyspace® analysis and how to analyze them. Here, <file> is an XML file that enumerates file sets and the behaviors that Polyspace uses with those files.

For instance, you can skip the definitions of function bodies in third-party libraries. When running a Bug Finder analysis, you can force analysis of all functions in files that you own.

If you run a verification:

  • At the command line, specify the absolute path to the XML files or path relative to the folder from which you run the command.

  • In the user interface (desktop products only), in the Other field, specify the option along with an absolute path to the XML or the path relative to the location of your Polyspace project. See Other.

A report generated from the analysis results only show the use of this option and not the details of which behaviors were associated with code elements.

A sample template file classification-template.xml shows the XML syntax. The file is in polyspaceroot\polyspace\verifier\cxx\ where polyspaceroot is the Polyspace installation folder.

You can associate a file classification with one or more products. That is, you can reuse the same classification XML file for a Bug Finder, Code Prover, and Polyspace as You Code analysis. Polyspace Code Prover™ supports a subset of classification XML syntax. For details about the syntax, see Classification XML File Syntax.

Examples

Exclude Generated Files in Bug Finder Analysis

Suppose your source code consists of the files utils.c, utils_generated.c, and header.h. Both .c files contain a comparison that incorrectly uses an = operator instead of the == operator.

  • src\utils.c:

    #include "header.h"

int getEvenElement(int *arr, int size, int idx) {
    int isIndexEven = isEven(idx);
    if(isIndexEven = 0 && idx < size)     // Invalid use of = operator
        return arr[idx];
    else
        return -1;
}

  • src\utils_generated.c:

    #include "header.h"

int isEven(int arg) {
    int rem = arg%2;
    if(rem = 0) {         // Invalid use of = operator
        return 1;
    }
    else {
        return 0;
    }
}

  • inc\header.h:

    int isEven(int);

Run the default Bug Finder analysis by using one of these commands:

  • polyspace-bug-finder -sources src\utils.c,src\utils_generated.c -I inc\
  • polyspace-bug-finder-server -sources src\utils.c,src\utils_generated.c -I inc\

You see an Invalid use of = operator defect in both .c files.

Suppose your generated files follow a naming convention and end with _generated. To exclude these files from analysis:

  1. Write a classification file that defines a set of files to exclude from analysis. The XML file excludes files with filename that end in _generated.

    <?xml version="1.0" encoding="UTF-8"?>

<specification>  
    <classification product="bug-finder">
       <fileset name="generated code">
            <files-in-set>
                <file-pattern>src/**/*_generated.c</file-pattern>
            </files-in-set>
            <behaviors>
                <do-not-analyze-functions>
                    <function-pattern>*</function-pattern>
                </do-not-analyze-functions>
                <show-results value="false"/>
            </behaviors>
        </fileset>
    </classification>
</specification>
    Specifying the pattern src/**/*_generated.c in the node file-pattern excludes all .c files in the src folder and all subfolders that have filenames that end in _generated.c. For more information on the syntax of classification XML files, see Classification XML File Syntax.

  2. Save the classification file as exclude_generated_files.xml. Specify this classification file with the option -classification by using one of these commands:

    • polyspace-bug-finder -sources src\utils.c,src\utils_generated.c -I inc\ -classification exclude_generated_files.xml
    • polyspace-bug-finder-server -sources src\utils.c,src\utils_generated.c -I inc\ -classification exclude_generated_files.xml

    Polyspace does not report the Invalid use of = operator defect utils_generated.c.

Exclude Functions from a Specific Namespace in Code Prover Analysis

Consider this code:

namespace NamespaceA {
	class Widget {
	public:
		int foo(int x) {
			return 42 / x;   // Division by zero 
		}
	};

}

namespace NamespaceB {
	class Gadget {
	public:
		int foo(int x) {
			return 42 / x;   // Division by zero  
		}
	};

}

int main() {
	volatile int rd = 0;
	if(rd) {
		NamespaceA::Widget w;
		w.foo(0);
	}
	if(rd) {
		NamespaceB::Gadget g;
		g.foo(0);
	}

}
If you run a default Code Prover analysis, functions in both namespaces are analyzed and Polyspace reports a red Division by zero (Polyspace Code Prover) check in NamespaceA::Widget::foo() and another one in NamesapceB::Gadget::foo().

To exclude functions from a specific namespace while running a Code Prover analysis:

  1. Write a classification XML file and define a set of file that encompasses all relevant files in the current analysis.

    <?xml version="1.0" encoding="UTF-8"?>

<specification>  
    <classification product="code-prover">
       <fileset name="all_files">
            <files-in-set>
                <file-pattern>$(source-files)</file-pattern>
            </files-in-set>
            <behaviors>
                <analyze-functions>
                    <function-pattern>$(all-relevant-functions)</function-pattern>
                </analyze-functions>
                <do-not-analyze-functions>
                    <function-pattern>::NamespaceA::</function-pattern>
                </do-not-analyze-functions>
                <show-results value="true"/>
            </behaviors>
        </fileset>
    </classification>
</specification>
    By specifying the function pattern $(all-relevant-functions) in the node analyze-functions, you specify that the analysis must analyze the called functions. You exclude the functions in namespace NamespaceA by using the pattern ::NamespaceA:: in the node do-not-analyze-function. For more information on the syntax of classification XML files, see Classification XML File Syntax.

  2. Save the classification file as classification_namespace_example.xml. Specify this classification file with the option -classification when you run a Code Prover analysis:

    polyspace-code-prover -sources src.cpp -classification classification_namespace_example.xml
    Polyspace no longer reports a red Division by zero check in NamespaceA::Widget::foo().

More About

expand all

Tips

Version History

Introduced in R2023a

expand all

See Also

Topics