polyspace.project.OwnedStaticAnalysisConfiguration Class

Namespace: polyspace.project

(Python) Static analysis configurations attached to specific project

Since R2024a

expand all in page

Description

The properties of the polyspace.project.OwnedStaticAnalysisConfiguration class contain the static analysis options attached to a specific Polyspace® Platform project. These properties correspond to the options related to static analysis in Polyspace Bug Finder™ and Polyspace Code Prover™. See Polyspace Bug Finder options (Polyspace Bug Finder) and Polyspace Code Prover options (Polyspace Code Prover).

To create modular projects, where project components like configurations and graphical tests are saved in separate files, consider using external configurations. An external configuration is a build, static analysis, or testing and profiling configuration that is saved in a separate .pscfg file that is referenced by the project. To work with external static analysis configurations in the Polyspace Python® API see polyspace.project.StaticAnalysisConfigurationRef and polyspace.project.StaticAnalysisConfiguration. For more information about project structure, see Modularize Project by Using External Configurations, Test References, and External Stub Files.

Creation

Syntax

staticAnalysisConfig = proj.StaticAnalysisConfigurations.create(configName)
staticAnalysisConfig = proj.StaticAnalysisConfigurations[configName]
staticAnalysisConfig = proj.StaticAnalysisConfigurations.createFrom(existingConfigObj)
staticAnalysisConfig = proj.StaticAnalysisConfigurations.createFrom(existingConfigObj, configName)
staticAnalysisConfig = proj.StaticAnalysisConfigurations.createFrom(existingConfigFile)
staticAnalysisConfig = proj.StaticAnalysisConfigurations.createFrom(existingConfigFile, configName)
staticAnalysisConfig = proj.StaticAnalysisConfigurations.moveAsOwned(existingConfigRefObj)

Description

Create Static Analysis Configuration

staticAnalysisConfig = proj.StaticAnalysisConfigurations.create(configName) creates a new polyspace.project.OwnedStaticAnalysisConfiguration object with the Name property set to configName and all other properties set to their default values. The resulting staticAnalysisConfig object is attached to the polyspace.project.Project object proj.

Load Static Analysis Configuration

staticAnalysisConfig = proj.StaticAnalysisConfigurations[configName] loads the existing polyspace.project.OwnedStaticAnalysisConfiguration object with the Name property set to configName from the polyspace.project.Project object proj.

Create Copy of Static Analysis Configuration

staticAnalysisConfig = proj.StaticAnalysisConfigurations.createFrom(existingConfigObj) creates a new polyspace.project.OwnedStaticAnalysisConfiguration object by copying an existing object existingConfigObj and attaches this copied object to the polyspace.project.Project object proj. To assign a unique name to staticAnalysisConfig, Polyspace uses the Name property of existingConfigObj and appends the next available numeric suffix.

staticAnalysisConfig = proj.StaticAnalysisConfigurations.createFrom(existingConfigObj, configName) creates a new polyspace.project.OwnedStaticAnalysisConfiguration object by copying an existing object existingConfigObj and attaches this copied object to the polyspace.project.Project object proj. Use the configName argument to set the Name property of the resulting object.

staticAnalysisConfig = proj.StaticAnalysisConfigurations.createFrom(existingConfigFile) creates a new polyspace.project.OwnedStaticAnalysisConfiguration object by copying the static analysis configuration defined in the file existingConfigFile.pscfg and attaches this object to the polyspace.project.Project object proj.

staticAnalysisConfig = proj.StaticAnalysisConfigurations.createFrom(existingConfigFile, configName) creates a new polyspace.project.OwnedStaticAnalysisConfiguration object by copying the static analysis configuration defined in the file existingConfigFile.pscfg, and attaches this object to the polyspace.project.Project object proj. Use the configName argument to set the Name property of the resulting object.

Convert Static Analysis Configuration

staticAnalysisConfig = proj.StaticAnalysisConfigurations.moveAsOwned(existingConfigRefObj) converts the static analysis configuration that the project proj references through existingConfigRefObj to a polyspace.project.OwnedStaticAnalysisConfiguration object and removes existingConfigRefObj from the project.

Input Arguments

expand all

Name of the static analysis configuration, specified as a string. This argument sets the Name property of the object.

Example: "My Static Analysis Configuration"

Existing owned static analysis configuration to make a copy of, specified as a polyspace.project.OwnedStaticAnalysisConfiguration object.

Example: proj.StaticAnalysisConfigurations[2]

Absolute or relative path to an existing .pscfg file, specified as a string. Relative paths are considered relative to the location of the .psprjx project file.

Example: "myStaticConfig.pscfg"

The existing referenced static analysis configuration that you want to convert to a polyspace.project.OwnedStaticAnalysisConfiguration object, specified as a polyspace.project.StaticAnalysisConfigurationRef object.

Example: proj.StaticAnalysisConfigurationRefs[0]

Properties

expand all

Name of the static analysis configuration, specified as a string. You can use this property to display the name of the configuration or assign a new name.

Example: staticConfig.Name

Example: staticConfig.Name="newConfigName"

Optional description of the static analysis configuration. Use this property to provide information about the static analysis configuration.

Example: "Static analysis configuration for mandatory MISRA C 2023 checks"

Specify commands or scripts to run after the analysis completes, or specify command-line-only options.

Specify the path of a command or script that Polyspace executes after the analysis completes. If you offload the analysis to a server machine, specify the path of the command or script on the server machine.

See also Command/script to apply after the end of the code verification (-post-analysis-command) (Polyspace Bug Finder).

Example: staticConf.Advanced.PostAnalysisCommand="/usr/local/scripts/postProcess.pl"

Specify additional static analysis options. For example, you might want to specify unofficial options provided by MathWorks® technical support to work around an issue.

To modify this property, use these methods:

  • append(optionName) — Add an additional analysis option.

  • pop(optionNameIdx) — Remove the analysis option with index optionNameIdx. If you do not specify an index, the last option in the list is removed.

  • clear() — Remove all additional analysis options.

See also Other (Polyspace Bug Finder).

Example: staticConf.Advanced.Other.append("-extra-flag otherOption")

Example: staticConf.Advanced.Other.pop(0)

Configure the behavior of Bug Finder checkers.

PropertyBehavior
AllowedPragmas

Specify the #pragma directives that Polyspace ignores when you enable one of these rules to check whether a #pragma is documented:

Polyspace reports a violation for any #pragma that is not specified with this option.

To modify this property, use these methods:

  • append(value) — Add a value to this property.

  • pop(valueIdx) — Remove the value with index valueIdx. If you do not specify an index, the last value in the list is removed.

  • clear() — Remove all values associated with this property.

Example: staticConf.BugFinderAnalysis.CheckersBehavior.AllowedPragmas.append("#pragma warning(disable : 1234"))

Example: staticConf.BugFinderAnalysis.CheckersBehavior.AllowedPragmas.pop(0)

See also Allowed pragmas (-allowed-pragmas) (Polyspace Bug Finder).

BooleanTypes

Specify data types that Polyspace treats as boolean when checking for certain coding rule violations. You can specify data types for this property only if you define those data types through an enum or typedef in your code.

To modify this property, use these methods:

  • append(value) — Add a value to this property.

  • pop(valueIdx) — Remove the value with index valueIdx. If you do not specify an index, the last value in the list is removed.

  • clear() — Remove all values associated with this property.

Example: staticConf.BugFinderAnalysis.CheckersBehavior.BooleanTypes.append("mybool_T")

Example: staticConf.BugFinderAnalysis.CheckersBehavior.BooleanTypes.pop(0)

For a list of coding rules checkers that are modified by this property, see Effective boolean types (-boolean-types) (Polyspace Bug Finder).

ChecksUsingSystemInputValues

Enable or disable stricter checks for system inputs. By default, this property is set to False. Set the property to True to enable it.

Example: staticConf.BugFinderAnalysis.CheckersBehavior.ChecksUsingSystemInputValues=True

See also Run stricter checks considering all values of system inputs (-checks-using-system-input-values) (Polyspace Bug Finder).

SystemInputsFrom

Specify the functions for which Polyspace runs stricter checks for system inputs. You can specify one of these values:

  • auto (default) — Consider all possible values for inputs to main() function and tasks, if any.

  • all — Consider all possible values for inputs to all functions.

  • uncalled — Consider all possible values for inputs to all uncalled functions.

  • custom — Provide a custom list of function names for Polyspace to check all possible input values. When you use this option, specify function names using the SystemInputsFromValues property.

To use this property, set ChecksUsingSystemInputValues to True.

Example: staticConf.BugFinderAnalysis.CheckersBehavior.SystemInputsFrom="uncalled"

See also Consider inputs to these functions (-system-inputs-from) (Polyspace Bug Finder).

SystemInputsFromValues

If you set the property SystemInputsFrom to custom, specify the list of functions for which Polyspace checks all possible system inputs.

To modify this property, use these methods:

  • append(functionName) — Add a function to the list.

  • pop(functionNameIdx) — Remove the function with index functionNameIdx. If you do not specify an index, the last function in the list is removed.

  • clear() — Remove all functions from the list.

Example: staticConf.BugFinderAnalysis.CheckersBehavior.SystemInputsFromValues.append("functionName")

Example: staticConf.BugFinderAnalysis.CheckersBehavior.SystemInputsFromValues.pop(0)

Enable the use of a custom selection of defect and coding rule checkers. By default, this property is set to False, and the Bug Finder analysis uses the default checkers selection. See Polyspace Bug Finder Defects Checkers Enabled by Default (Polyspace Bug Finder).

If you enable this property, use CheckersActivationFile to specify the path of the XML file where you store your custom selection of defect and coding rule checkers.

Example: staticConf.BugFinderAnalysis.EnableCheckersActivationFile=True

Specify the path of the checkers activation file when you set EnableCheckersActivationFile to True. To view the available defects and coding rule checkers, see Polyspace Bug Finder Results (Polyspace Bug Finder).

For more on how to create and edit the checkers activation file, see Checkers activation file (-checkers-activation-file) (Polyspace Bug Finder).

Example: staticConf.BugFinderAnalysis.CheckersActivationFile="/usr/local/checkersFile.xml"

If you project contains generated code, enable this property to check the compliance of the code with the MISRA C:2012 coding standard.

See also Use generated code requirements (-misra3-agc-mode) (Polyspace Bug Finder).

Example: staticConf.BugFinderAnalysis.Misra3AgcMode=True

If you project contains generated code, enable this property to check the compliance of the code with the MISRA C:2023 coding standard.

See also Use generated code requirements (-misra-c-2023-agc-mode) (Polyspace Bug Finder).

Example: staticConf.BugFinderAnalysis.MisraC2023AgcMode=True

Enable this property to calculate code complexity metrics for your project. To view a list of code metrics that Polyspace Bug Finder calculates, see HIS Code Complexity Metrics (Polyspace Bug Finder).

See also Calculate code metrics (-code-metrics) (Polyspace Bug Finder).

Example: staticConf.BugFinderAnalysis.CodeMetrics=True

Specify the files for which Polyspace generates analysis results. Files for which Polyspace does not generate results are not excluded from the analysis. Use this property to, for example, suppress results from third party library header files that you include in your code. The available values are:

  • "all-headers" — Polyspace generates results for all source files and all header files. The header files can be in the same folder as source files, in subfolders of source file folders or in include folders.

  • "source-headers" (default) — Polyspace generates results for the source files and the header files that are in the same folder as the source files or in subfolders of source file folders.

  • "custom" — Polyspace generates results for the source files and the folders that you specify. If you enter a folder name, results appear on header files in that folder (and its subfolders).

    Use GenerateResultsForValues to specify the file and folder paths.

See also Generate results for sources and (-generate-results-for) (Polyspace Bug Finder).

Example: staticConf.BugFinderAnalysis.GenerateResultsFor="custom"

If you set GenerateResultsFor to custom, use this property to specify the list of files and folders for which Polyspace generates results.

To modify this property, use these methods:

  • append(path) — Add a file or folder path to this property.

  • pop(pathIdx) — Remove the file or folder path with index pathIdx. If you do not specify an index, the last item in the list is removed.

  • clear() — Remove all file and folder paths associated with this property.

Example: staticConf.BugFinderAnalysis.GenerateResultsForValues.append("/path/to/myfile.c")

Example: staticConf.BugFinderAnalysis.GenerateResultsForValues.append("/path/to/folder")

Example: staticConf.BugFinderAnalysis.GenerateResultsForValues.pop(0)

Specify the files for which Polyspace does not generate analysis results. Files for which Polyspace does not generate results are not excluded from the analysis. Use this property to, for example, suppress results from header files that are in the same folder as the analyzed source files. The available values are:

  • all-headers — Polyspace does not generate results for all header files. The header files can be in the same folder as source files, in subfolders of source file folders or in include folders.

  • source-headers (default) — Polyspace does not generate results for header files in include folders (and their subfolders).

  • custom — Polyspace does not generate results for the files and folders that you specify. If you enter a folder name, results are suppressed from files in that folder (and its subfolders).

    Use DoNotGenerateResultsForValues to specify the file and folder paths.

See also Do not generate results for (-do-not-generate-results-for) (Polyspace Bug Finder).

Example: staticConf.BugFinderAnalysis.DoNotGenerateResultsFor="source-headers"

If you set DoNotGenerateResultsFor to custom, use this property to specify the list of files and folders for which Polyspace does not generate results.

To modify this property, use these methods:

  • append(path) — Add a file or folder path to this property.

  • pop(pathIdx) — Remove the file or folder path with index pathIdx. If you do not specify an index, the last item in the list is removed.

  • clear() — Remove all file and folder paths associated with this property.

Example: staticConf.BugFinderAnalysis.DoNotGenerateResultsForValues.append("/path/to/folder")

Example: staticConf.BugFinderAnalysis.DoNotGenerateResultsForValues.pop(0)

Use these properties to modify the default behavior of run-time checks during a Code Prover verification. For example, specify that Polyspace check for overflows in computations that use unsigned integers in addition to the default behavior of checking for overflows in computations that use signed integers.

PropertyBehavior
AllowNegativeOperandInShift

Specify that a Code Prover verification allows left shift operations on negative numbers. By default, this property is set to False and Code Prover produces a red check on this type of operation.

Example: staticConf.CodeProverVerification.CheckBehavior.AllowNegativeOperandInShift=True

See also Allow negative operand for left shifts (-allow-negative-operand-in-shift) (Polyspace Code Prover).

AllowNonFiniteFloats

Enable analysis mode that incorporates Infinites and NaNs for floating point operations. By default, this property is set to False

See also Consider non finite floats (-allow-non-finite-floats) (Polyspace Code Prover).

Example: staticConf.CodeProverVerification.CheckBehavior.AllowNonFiniteFloats=True

AllowPtrArithOnStruct

Specify that a pointer assigned to a structure field can point outside its bounds as long as it points within the structure. By default, this property is set to False.

Example: staticConf.CodeProverVerification.CheckBehavior.AllowPtrArithOnStruct=True

See also Enable pointer arithmetic across fields (-allow-ptr-arith-on-struct) (Polyspace Code Prover).

CheckGlobalsInit

Specify that Polyspace must check whether all non-const global variables (and local static variables) are explicitly initialized at declaration or within a section of code marked as initialization code. By default, this property is set to False.

Example: staticConf.CodeProverVerification.CheckBehavior.CheckGlobalsInit=True

See also Check that global variables are initialized after warm reboot (-check-globals-init) (Polyspace Code Prover).

CheckInfinite

Specify how the analysis handles floating-point operations that result in infinities. The available values are:

  • allow (default) — Polyspace does not report a run-time error on floating-point operations that result in infinities.

  • warn-first — Polyspace reports a run-time error on operations that result in an infinite when the operands themselves are not infinite. The verification does not terminate the execution thread that produces infinity.

  • forbid — Polyspace reports a run-time error on the operation and terminates the execution thread that produces infinity.

Example: staticConf.CodeProverVerification.CheckBehavior.CheckInfinite="warn-first"

See also Infinities (-check-infinite) (Polyspace Code Prover).

CheckNan

Specify how the analysis handles floating-point operations that result in NaNs. The available values are:

  • allow (default) — Polyspace does not report a run-time error on floating-point operations that result in NaN.

  • warn-first — Polyspace reports a run-time error on operations that result in a NaN when the operands themselves are not NaN. The verification does not terminate the execution thread that produces NaN.

  • forbid — Polyspace reports a run-time error on the operation and terminates the execution thread that produces NaN.

See also NaNs (-check-nan) (Polyspace Code Prover).

Example: staticConf.CodeProverVerification.CheckBehavior.CheckNan="forbid"

CheckSubnormal

Specify how the analysis handles floating-point operations that result in subnormal values. The values indicate a loss of significant digits. You can set this property to:

  • allow (default) — Polyspace does not checks for subnormal floating-point results.

  • forbid — Polyspace checks for subnormal results, stops the execution path with the subnormal result, and prevents subnormal values from propagating further.

  • warn-all — Polyspace checks for and highlights all occurrences of subnormal results.

  • warn-first — Polyspace checks for and highlights the first occurrence of a subnormal result. If a subnormal value propagates to further subnormal results, those subsequent results are not highlighted.

Example: staticConf.CodeProverVerification.CheckBehavior.CheckSubnormal="warn-first"

See also Subnormal detection mode (-check-subnormal) (Polyspace Code Prover).

DetectPointerEscape

Specify that Polyspace detects cases where you access a variable outside its scope via dangling pointers. By default, this property is set to False.

Example: staticConf.CodeProverVerification.CheckBehavior.DetectPointerEscape=True

See also Detect stack pointer dereference outside scope (-detect-pointer-escape) (Polyspace Code Prover).

DisableInitializationChecks

Specify that Polyspace does not check for non-initialized variables and pointers. By default, this property is set to False.

Example: staticConf.CodeProverVerification.CheckBehavior.DisableInitializationChecks=True

See also Disable checks for non-initialization (-disable-initialization-checks) (Polyspace Code Prover).

ImpactAnalysis

Specify that Polyspace checks for the presence or absence of impact between program elements designated as sources and sinks. Use the property ImpactSpecifications to specify the source-sink pairs. By default, this property is set to False

See also Enable impact analysis (-impact-analysis) (Polyspace Code Prover).

Example: staticConf.CodeProverVerification.CheckBehavior.ImpactAnalysis=True

ImpactAnalysisOnly

Specify that Polyspace checks for only the presence or absence of impact between program elements designated as sources and sinks. If you enable this property Polyspace skips the Code Prover analysis for run-time errors. By default, this property is set to False.

To use this property, set ImpactAnalysis to True and use ImpactSpecifications to specify the source-sink pairs.

Example: staticConf.CodeProverVerification.CheckBehavior.ImpactAnalysisOnly=True

See also Show impact analysis results only (-impact-analysis-only) (Polyspace Code Prover).

ImpactSpecifications

Specify the path of the XML file where you define the source-sink pairs for which Polyspace performs and impact analysis. To use this property, set ImpactAnalysis to True.

Example: staticConf.CodeProverVerification.CheckBehavior.ImpactSpecifications="/path/to/myFile.xml"

For more information on creating and editing the XML file where you define source-sink pairs, see Specify sources and sinks (-impact-specifications) (Polyspace Code Prover).

PermissiveFunctionPointer

Specify that Polyspace allows function pointer calls where the type of the function pointer does not match the type of the function. By default, this property is set to False.

Example: staticConf.CodeProverVerification.CheckBehavior.PermissiveFunctionPointer=True

See also Permissive function pointer calls (-permissive-function-pointer) (Polyspace Code Prover).

SignedIntegerOverflows

Specify how the analysis handles signed integer overflows. The available values are:

  • forbid (default) — Polyspace checks for and reports signed integer overflows.

  • allow — Polyspace does not report signed integer overflows run-time errors. If an operation results in an overflow, Polyspace wraps the result of the overflow.

  • warn-with-wrap-around — Polyspace reports signed integer overflows run-time errors. If an operation results in an overflow, Polyspace wraps the result of the overflow.

See also Overflow mode for signed integer (-signed-integer-overflows) (Polyspace Code Prover).

Example: staticConf.CodeProverVerification.CheckBehavior.SignedIntegerOverflows="allow"

SizeInBytes

Specify that Polyspace allows dereferencing a pointer that points to a structure, but the pointer has a sufficient buffer for only some of the structure’s fields. By default, this property is set to False.

Example: staticConf.CodeProverVerification.CheckBehavior.SizeInBytes=True

See also Allow incomplete or partial allocation of structures (-size-in-bytes) (Polyspace Code Prover).

StackUsage

Specify that Polyspace computes and displays the stack usage of your source code. By default, this property is set to False.

Example: staticConf.CodeProverVerification.CheckBehavior.StackUsage=True

See also Calculate stack usage (-stack-usage) (Polyspace Code Prover).

UncalledFunctionChecks

Specify that Polyspace detects functions that are not called directly or indirectly from main or another entry point function during run-time. The available values are:

  • none (default) — Polyspace does not check for uncalled functions.

  • never-called — Polyspace checks for functions that are defined but not called.

  • called-from-unreachable — Polyspace checks for functions that are defined and called from an unreachable part of the code.

  • all — Polyspace checks for functions that are defined but not called, and function that are defined and called from an unreachable part of the code.

Example: staticConf.CodeProverVerification.CheckBehavior.UncalledFunctionChecks="all"

See also Detect uncalled functions (-uncalled-function-checks) (Polyspace Code Prover).

UnsignedIntegerOverflows

Specify how the analysis handles unsigned integer overflows. The available values are:

  • allow (default) — Polyspace does not report unsigned integer overflows run-time errors. If an operation results in an overflow, Polyspace wraps the result of the overflow.

  • forbid — Polyspace checks for and reports unsigned integer overflows.

  • warn-with-wrap-around — Polyspace reports unsigned integer overflows run-time errors. If an operation results in an overflow, Polyspace wraps the result of the overflow.

Example: staticConf.CodeProverVerification.CheckBehavior.UnsignedIntegerOverflows="forbid"

See also Overflow mode for unsigned integer (-unsigned-integer-overflows) (Polyspace Code Prover).

Specify the classes that Polyspace uses to generate a main() function. By default, Polyspace uses all classes that have at least one method defined outside a header file. Polyspace generates a main() function only if one does not already exist. Otherwise, Polyspace uses the existing main() function.

To generate a main() that does not call any class method, set the property to none.

To generate a main() that uses a custom list of classes, set the property to custom and use ClassAnalyzerValues to specify the list of classes.

See also Class (-class-analyzer) (Polyspace Bug Finder).

Example: ataticConf.CodeProverVerification.ClassAnalyzer="custom"

Specify the class methods that Polyspace uses to generate a main() function. You can specify one of these values:

  • "all" — The generated main calls all public and protected methods. It does not call methods inherited from a parent class.

  • "all-public" — The generated main calls all public methods. It does not call methods inherited from a parent class.

  • "inherited-all" — The generated main calls all public and protected methods including those inherited from a parent class.

  • "inherited-all-public" — The generated main calls all public methods including those inherited from a parent class.

  • "unused" (default) — The generated main calls public and protected methods that are not called in the code.

  • "unused-public" — The generated main calls public methods that are not called in the code. It does not call methods inherited from a parent class.

  • "inherited-unused" — The generated main calls public and protected methods that are not called in the code including those inherited from a parent class.

  • "inherited-unused-public" — The generated main calls public methods that are not called in the code including those inherited from a parent class.

  • "custom" — The generated main calls the methods that you specify. Use ClassAnalyzerCallsValues to specify the custom list of class methods.

See also Functions to call within the specified classes (-class-analyzer-calls) (Polyspace Bug Finder).

Example: staticConf.CodeProverVerification.ClassAnalyzerCalls="all-public"

If you set ClassAnalyzerCalls to custom, use this property to specify a list of class methods that Polyspace uses to generate a main. Polyspace analyzes only methods that are called directly or indirectly from the main function.

To modify this property, use these methods:

  • append(value) — Add a value to this property.

  • pop(valueIdx) — Remove the value with index valueIdx. If you do not specify an index, the last item in the list is removed.

  • clear() — Remove all values associated with this property.

Example: staticConf.CodeProverVerification.ClassAnalyzerCallsValues.append("myClass::myMethod()")

Example: staticConf.CodeProverVerification.ClassAnalyzerCallsValues.append("myClass::myMethodWithParams(int, int)")

Example: staticConf.CodeProverVerification.ClassAnalyzerCallsValues.pop(0)

If you set ClassAnalyzer to custom, use this property to specify a list of classes that Polyspace uses to generate a main, and then use ClassAnalyzerCalls to specify the methods that the main calls. Polyspace analyzes only methods that are called directly or indirectly from the main function.

To modify this property, use these methods:

  • append(value) — Add a value to this property.

  • pop(valueIdx) — Remove the value with index valueIdx. If you do not specify an index, the last item in the list is removed.

  • clear() — Remove all values associated with this property.

Example: staticConf.CodeProverVerification.ClassAnalyzerValues.append("myClass")

Example: staticConf.CodeProverVerification.ClassAnalyzerValues.pop(0)

Specify that Polyspace analyze only the methods of classes that you specify with the properties ClassAnalyzer and ClassAnalyzerCalls. By default, this property is set to False.

See also Analyze class contents only (-class-only) (Polyspace Bug Finder).

Example: staticConf.CodeProverVerification.ClassOnly=True

Specify the functions that the generated main() function calls ahead of other functions. Polyspace generates a main() function only if one does not already exist. Otherwise, Polyspace uses the existing main() function.

To modify this property, use these methods:

  • append(value) — Add a value to this property.

  • pop(valueIdx) — Remove the value with index valueIdx. If you do not specify an index, the last item in the list is removed.

  • clear() — Remove all values associated with this property.

See also Initialization functions (-functions-called-before-main) (Polyspace Bug Finder).

Example: staticConf.CodeProverVerification.FunctionsCalledBeforeMain.append("myClass::myMethod()")

Example: staticConf.CodeProverVerification.FunctionsCalledBeforeMain.append("myClass::myMethodWithParams(int, int)")

Example: staticConf.CodeProverVerification.FunctionsCalledBeforeMain.pop(0)

Specify that Polyspace checks only the section of the code marked as initialization code for run-time errors and other issues.

See also Verify initialization section of code only (-init-only-mode) (Polyspace Bug Finder).

Example: staticConf.CodeProverVerification.InitOnlyMode=True

Specify a Microsoft Visual C++ extension of main that the program uses as a main function.

The extensions provide additional capabilities beyond the standard main function.

See also Main entry point (-main) (Polyspace Bug Finder).

Example: staticConf.CodeProverVerification.Main="DllMain"

Specify that Polyspace generates a main() function if one does not already exist, for example, if you analyze a module or library. If a main() function already exists, the analysis uses that main() function instead.

Set this property to False to stop the analysis if no main() function exists.

See also Verify module or library (-main-generator) (Polyspace Bug Finder).

Example: staticConf.CodeProverVerification.MainGenerator=False

Specify the functions that the generated main() calls after the functions you specify with the property FunctionsCalledBeforeMain. You can specify one of these values:

  • none — The generated main() does not call any function.

  • unused (default) — The generated main() calls only functions that are not called anywhere else in the source code, except if those functions are inline.

  • all — The generated main() calls all the functions except for inlined functions.

  • custom — The generated main() calls the functions that you specify with the property MainGeneratorCallsValues.

See also Functions to call (-main-generator-calls) (Polyspace Bug Finder).

Example: staticConf.CodeProverVerification.MainGeneratorCalls="all"

Specify a custom list of functions that the generated main() calls after the functions you specify with the property FunctionsCalledBeforeMain.

To modify this property, use these methods:

  • append(value) — Add a value to this property.

  • pop(valueIdx) — Remove the value with index valueIdx. If you do not specify an index, the last item in the list is removed.

  • clear() — Remove all values associated with this property.

Example: staticConf.CodeProverVerification.MainGeneratorCallsValues.append("myClass::myMethod()")

Example: staticConf.CodeProverVerification.MainGeneratorCallsValues.append("myClass::myMethodWithParams(int, int)")

Example: staticConf.CodeProverVerification.MainGeneratorCallsValues.pop(0)

Specify the global variables that the generated main() function initializes. Polyspace considers that these variables to have any value allowed by their type. You can specify one of these values:

  • none — The generated main() does not initialize global variables.

  • public (default) — The generated main() initializes all global variables except for variables declared with a static or const keyword.

  • uninit — The generated main() initializes only global variables that are not initialized when they are declared.

  • all — The generated main() initializes all global variables except for variables declared with const keyword.

  • custom — The generated main() initializes the global variables that you specify with the property MainGeneratorWritesVariablesValues

See also Variables to initialize (-main-generator-writes-variables) (Polyspace Bug Finder).

Example: staticConf.CodeProverVerification.MainGeneratorWritesVariables="uninit"

If you set the property MainGeneratorWritesVariablesValues to custom, use this property to specify the custom list of global variables that the generated main() initializes.

To modify this property, use these methods:

  • append(value) — Add a value to this property.

  • pop(valueIdx) — Remove the value with index valueIdx. If you do not specify an index, the last item in the list is removed.

  • clear() — Remove all values associated with this property.

Example: staticConf.CodeProverVerification.MainGeneratorWritesVariablesValues.append("globVar")

Example: staticConf.CodeProverVerification.MainGeneratorWritesVariablesValues.pop(0)

Specify that Polyspace does not check whether each class constructor initializes all class members.

See also Skip member initialization check (-no-constructors-init-check) (Polyspace Bug Finder).

Example: staticConf.CodeProverVerification.NoConstructorsInitCheck=True

Use these properties to modify the precision of the Code Prover verification. A more precise verification results in fewer orange checks. These checks indicate code where the verification cannot prove the presence or absence of an error.

PropertyBehavior
ContextSensitivity

Specify the functions for which Polyspace stores the call context information. If a function is called multiple times, you can use this information to identify the function call that caused an error. The available values are:

  • none (default) — Polyspace does not store call context information for functions.

  • auto — Polyspace stores call context information for checks in:

    • Functions that form the leaves of the call tree. These functions are called by other functions, but do not call functions themselves.

    • Small functions. The software uses an internal threshold to determine whether a function is small.

  • custom — Polyspace stores the call context information for the functions that you specify with the property ContextSensitivityValues.

that a Code Prover verification allows left shift operations on negative numbers. By default, this property is set to False and Code Prover produces a red check on this type of operation.

Example: staticConf.CodeProverVerification.Precision.ContextSensitivity="auto"

See also Sensitivity context (-context-sensitivity) (Polyspace Code Prover).

ContextSensitivityValues

If you set ContextSensitivity to custom, use this property to specify the list of function for which Polyspace stores the call context information.

See also Sensitivity context (-context-sensitivity) (Polyspace Code Prover).

To modify this property, use these methods:

  • append(value) — Add a value to this property.

  • pop(valueIdx) — Remove the value with index valueIdx. If you do not specify an index, the last item in the list is removed.

  • clear() — Remove all values associated with this property.

Example: staticConf.CodeProverVerification.Precision.ContextSensitivityValues.append("myClass::myFunc()")

Example: staticConf.CodeProverVerification.Precision.ContextSensitivityValues.pop(0)

ModulesPrecision

Specify the path of source files whose code you want to verify at a higher precision level than the rest of the verification.

To modify this property, use these methods:

  • append(filepath:precision) — Add a value to this property.

  • pop(filepath:precisionIdx) — Remove the value with index filepath:precisionIdx. If you do not specify an index, the last item in the list is removed.

  • clear() — Remove all values associated with this property.

Example: staticConf.CodeProverVerification.Precision.ModulesPrecision.append("/path/to/file.c:O3")

Example: staticConf.CodeProverVerification.Precision.ModulesPrecision.pop(0)

See also Specific precision (-modules-precision) (Polyspace Code Prover). For more on precision levels, see Precision level (-O0 | -O1 | -O2 | -O3) (Polyspace Code Prover)

PathSensitivityDelta

Specify that Polyspace uses fewer approximations when verifying code with fewer lines (less than 1000 lines of code.

By default, this property is set to 0, which corresponds to off. To enable the property, specify a positive integer. Larger integers results in more precision but also longer verification times.

Example: staticConf.CodeProverVerification.Precision.PathSensitivityDelta=5

See also Improve precision of interprocedural analysis (-path-sensitivity-delta) (Polyspace Code Prover).

PrecisionLevel

Specify a precision level for the verification. A higher precision produces fewer orange checks but results in a longer verification time. You can assign one of these precision levels, where each level corresponds to a different verification algorithm:

  • 0 — Verification uses a static interval verification

  • 1 — Verification uses a more complex static interval verification compared to level 0.

  • 2 (default) — Verification uses a complex polyhedron model of domain values with additional precision for interprocedural analysis

  • 3 — This precision level is suitable only for code having less than 1000 lines. Using this option, the percentage of proven results can be very high.

Example: staticConf.CodeProverVerification.CheckBehavior.CheckInfinite="warn-first"

See also Precision level (-O0 | -O1 | -O2 | -O3) (Polyspace Code Prover).

To

Specify the number of times the verification process runs on your code. Each additional run can lead to a greater number of proven results but also a longer verification time. You can assign one of these values:

  • Source Compliance Checking — Polyspace checks for only compilation errors. Most coding rule violations are found at this verification level.

  • Software Safety Analysis level 0 — The verification process performs some simple analysis. The analysis is designed to reach completion despite complexities in the code.

  • Software Safety Analysis level 1 — The verification process analyzes each function once with algorithms whose complexity depends on the precision level.

  • Software Safety Analysis level 2 (default) — The verification process analyzes each function twice. In the first pass, the analysis propagates from the top of the function call hierarchy to the leaves. In the second pass, the analysis propagates from the leaves back to the top. Each pass uses information gathered from the previous pass.

  • Software Safety Analysis level 3 — The verification process runs three times on each function: from the top of the function call hierarchy to the leaves, from the leaves to the top, and from the top to the leaves again. Each pass uses information gathered from the previous pass.

  • Software Safety Analysis level 4 — The verification process runs four passes on each function: from the top of the function call hierarchy to the leaves twice. Each pass uses information gathered from the previous pass.

  • other — If you use this option, Polyspace verification will make 20 passes unless you stop it manually.

See also Verification level (-to) (Polyspace Code Prover).

Example: staticConf.CodeProverVerification.Precision.To="Source Compliance Checking"

Use these properties to perform a deeper or more superficial analysis of specific code constructs. Changing these properties can significantly affect verification time.

PropertyBehavior
EnableKLimiting

Enable limiting the depth of the analysis for nested structures. By default, this property is set to False.

Example: staticConf.CodeProverVerification.Scaling.EnableKLimiting=True

See also Depth of verification inside structures (-k-limiting) (Polyspace Code Prover).

KLimiting

Specify the depth of the analysis for nested structures. Use this property if you set the property EnableKLimiting to True.

By default, this property is set to 0 which corresponds to no verification of structures inside other structures. Specify a positive integer that corresponds to the depth of analysis for nested structures. A number less than 2 can result in a less precise verification.

Example: staticConf.CodeProverVerification.Scaling.KLimiting=4

See also Depth of verification inside structures (-k-limiting) (Polyspace Code Prover).

Inline

Specify the functions that Polyspace clones internally for each function call. The cloning can help reduce the complexity of the code.

To modify this property, use these methods:

  • append(functionName) — Add a function to this property.

  • pop(functionNameIdx) — Remove the function with index functionNameIdx. If you do not specify an index, the last function in the list is removed.

  • clear() — Remove all values associated with this property.

Example: staticConf.CodeProverVerification.Scaling.Inline.append("myFunc()")

Example: staticConf.CodeProverVerification.Scaling.Inline.pop(0)

See also Inline (-inline) (Polyspace Code Prover).

Specify that Polyspace runs a less extensive analysis that computes only the global variables sharing and usage in your entire application.

See also Show global variable sharing and usage only (-shared-variables-mode) (Polyspace Code Prover).

Example: staticConf.CodeProverVerification.SharedVariablesMode=True

Specify that Polyspace verifies each source file individually and independently from other source files in your application.

See also Verify files independently (-unit-by-unit) (Polyspace Code Prover).

Example: staticConf.CodeProverVerification.UnitByUnit=True

Specify the files that Polyspace includes with each file when running a file-by-file verification. The files that you specify are compiled once and then linked to each file verification.

To modify this property, use these methods:

  • append(filePath) — Add a file to this property.

  • pop(filePathIdx) — Remove the file with index filePathIdx. If you do not specify an index, the last file in the list is removed.

  • clear() — Remove all files associated with this property.

See also Common source files (-unit-by-unit-common-source) (Polyspace Code Prover).

Example: staticConf.CodeProverVerification.UnitByUnitCommonSource.append("/path/to/file.c")

Example: staticConf.CodeProverVerification.UnitByUnitCommonSource.pop(0)

Specify global assumptions that Polyspace makes about specific code constructs during the analysis.

PropertyBehavior
ConsiderVolatileQualifierOnFields

Specify that a Code Prover verification takes into account the volatile qualifier on the fields of a structure. By default, this property is set to False.

Example: staticConf.CodeProverVerification.VerificationAssumption.ConsiderVolatileQualifierOnFields=True

See also Consider volatile qualifier on fields (-consider-volatile-qualifier-on-fields) (Polyspace Code Prover).

FloatRoundingMode

Specify the rounding mode Polyspace uses to determine the results of floating-point arithmetic operations. Specify one of these values:

  • to-nearest (default) — Polyspace uses "to-nearest" rounding for operations that use floating point variables.

  • all — Polyspace checks the results of each operation involving floating-point variables using these rounding modes: round-to-nearest, round-towards-zero, round-towards-positive-infinity, and round-towards-negative-infinity.

See also Float rounding mode (-float-rounding-mode) (Polyspace Code Prover).

Example: staticConf.CodeProverVerification.VerificationAssumption.FloatRoundingMode="all"

IgnoreAssemblyCode

Specify that assembly instructions in C/C++ code cannot modify C/C++ variables. By default, this property is set to False.

Example: staticConf.CodeProverVerification.VerificationAssumption.IgnoreAssemblyCode=True

See also Ignore assembly code (-ignore-assembly-code) (Polyspace Code Prover).

UnconstrainedPointersMayBeNull

Specify that environment pointers, which are pointers that can be assigned values outside your code, can have a NULL value. By default, this property is set to False.

Example: staticConf.CodeProverVerification.VerificationAssumption.UnconstrainedPointersMayBeNull=True

See also Consider environment pointers as unsafe (-stubbed-pointers-are-unsafe) (Polyspace Code Prover).

Specify a time out limit in hours beyond which the analysis stops if it does not complete. Use this option to modify the default time out limit for an analysis. A Code Prover analysis times out if an internal step in the analysis lasts more than 24 hours. Use decimals to specify fractions of an hour.

See also Verification time limit (-timeout) (Polyspace Code Prover).

Example: staticConf.ComputingSettings.Timeout="5.75"

Specify that DOS or Windows® files are provided for analysis. Enable this property to help resolve case sensitivity and control character issues.

See also Code from DOS or Windows file system (-dos) (Polyspace Bug Finder).

Example: staticConf.EnvironmentSettings.Dos=True

Specify the path of an executable file or script that Polyspace runs on each source file after the preprocessing phase of the analysis. Use a post processing command to work around compilation errors or imprecisions in the analysis without modifying your source code.

See also Command/script to apply to preprocessed files (-post-preprocessing-command) (Polyspace Bug Finder).

Example: staticConf.EnvironmentSettings.PostPreprocessingCommand="/path/to/script.sh

Specify that the analysis stops if there are any compilation errors.

See also Stop analysis if a file does not compile (-stop-if-compile-error) (Polyspace Bug Finder).

Example: staticConf.EnvironmentSettings.StopIfCompileError=True

Specify the path of an XML file where you specify constraints on the value of global variables, functions inputs, and the return values of stubbed functions.

For more information on creating and editing the XML file, see Constraint setup (-data-range-specifications) (Polyspace Bug Finder).

Example: staticConf.InputsStubbing.DataRangeSpecifications="/path/to/constraints.xml"

Specify the name of functions that Polyspace stubs during an analysis. Polyspace ignores the definition of a stubbed function and assumes the function inputs and outputs have full range of values allowed by their type.

To modify this property, use these methods:

  • append(functionName) — Add a function to this property.

  • pop(functionNameIdx) — Remove the file with index functionNameIdx. If you do not specify an index, the last function in the list is removed.

  • clear() — Remove all functions associated with this property.

See also Functions to stub (-functions-to-stub) (Polyspace Bug Finder).

Example: staticConf.InputsStubbing.FunctionsToStub.append("myFunc()")

Example: staticConf.InputsStubbing.FunctionsToStub.pop(0)

Specify the library that you use in your program. Polyspace uses smart stubs for functions from those libraries instead of generic stubs and does not attempt to check the function implementations. You can specify one of these libraries:

  • none — The analysis uses smart stubs only for functions from the C Standard Library.

  • autosar — The analysis uses smart stubs for AUTOSAR RTE API functions even if their implementations are available.

  • stdlibcxx — The analysis uses smart stubs for methods from C++ Standard Library containers even if their implementations are available.

See also Libraries used (-library) (Polyspace Bug Finder).

Example: staticConf.InputsStubbing.Library="autosar"

Specify that the analysis considers global and static variables as uninitialized unless those variables are explicitly initialized in the code.

See also Ignore default initialization of global variables (-no-def-init-glob) (Polyspace Bug Finder).

Example: staticConf.InputsStubbing.NoDefInitGlob=True

Configure Polyspace to identify certain families of multitasking functions, or use the relevant Multitasking properties to explicitly specify the entry points, cyclic tasks, interrupts, and protection mechanisms for shared variables in your code.

Specify the path of the ARXML file that Polyspace parses to setup the multitasking configuration for your AUTOSAR project.

Polyspace parses the ARXML files that you provide for OsTask, OsIsr, OsResource, OsAlarm, and OsEvent definitions. The analysis uses these definitions and the supported multitasking keywords to configure tasks, interrupts, cyclical tasks, and critical sections.

To modify this property, use these methods:

  • append(ARXMLPath) — Add a value to this property.

  • pop(ARXMLPathIdx) — Remove the value with index ARXMLPathIdx. If you do not specify an index, the last value in the list is removed.

  • clear() — Remove all values associated with this property.

See also ARXML files selection (-autosar-multitasking) (Polyspace Bug Finder).

Example: staticConf.Multitasking.AutosarMultitasking.append("/path/to/autosar.arxml")

Example: staticConf.Multitasking.AutosarMultitasking.pop(0)

Use a polyspace.project.CriticalSection object to specify the functions that begin and end a critical section in your code.

For example, if your code has a critical section that begins with the function myLock and ends with the function myUnlock, create a critical section object and then append it to the CriticalSections property to define the critical section.

# Define critical section object
cs = polyspace.project.CriticalSection
# Declare functions that begin and end the critical section and append the 
# critical section object to the CriticalSections property
staticConf.Multitasking.CriticalSections.append(cs(Begin="myLock",End="myUnLock"))

To modify this property, use these methods:

  • append(criticalSectionObject) — Add a polyspace.project.CriticalSection object to this property.

  • pop(criticalSectionObjectIdx) — Remove the polyspace.project.CriticalSection object with index criticalSectionObjectIdx. If you do not specify an index, the last polyspace.project.CriticalSection object in the list is removed.

    Display the available critical sections (staticConf.Multitaksing.CriticalSections to obtain the index of the critical section that you want to remove.

  • clear() — Remove all polyspace.project.CriticalSection objects associated with this property.

See also Critical section details (-critical-section-begin -critical-section-end) (Polyspace Bug Finder).

Specify the name of the functions that correspond to cyclic tasks in your code.

To modify this property, use these methods:

  • append(functionName) — Add a function to this property.

  • pop(functionNameIdx) — Remove the function with index functionNameIdx. If you do not specify an index, the last function in the list is removed.

  • clear() — Remove all functions associated with this property.

See also Cyclic tasks (-cyclic-tasks) (Polyspace Bug Finder).

Example: staticConf.Multitasking.CyclicTasks.append("funcIsCyclicTask")

Example: staticConf.Multitasking.CyclicTasks.pop(0)

Specify that Polyspace generates a report after the analysis completes.

See also Generate report (Polyspace Bug Finder).

Example: staticConf.Reporting.EnableReportGeneration=True

Specify the format of the generated report. Polyspace can generate and save a report to one of these file formats: HTML, PDF, or WORD.

See also Output format (-report-output-format) (Polyspace Bug Finder).

Example: staticConf.Reporting.ReportOutputFormat="PDF"

Specify the name of the report template you use to generate a report for Bug Finder analysis results.

For a description of the content of each report template, see Bug Finder and Code Prover report (-report-template) (Polyspace Bug Finder).

To use this property, set EnableReportGeneration to True.

Example: staticConf.Reporting.ReportTemplateBugFinder="CodingStandards"

Specify the name of the report template you use to generate a report for Code Prover analysis results.

For a description of the content of each report template, see Bug Finder and Code Prover report (-report-template) (Polyspace Bug Finder).

To use this property, set EnableReportGeneration to True.

Example: staticConf.Reporting.ReportTemplateCodeProver="DeveloperReview"

Methods

expand all

Version History

Introduced in R2024a

expand all

See Also

| | | | | |

Topics