Polyspace Code Prover Options in Polyspace Platform User Interface

You can run static analysis on C/C++ code in the Polyspace Platform user interface:

Using Polyspace^® Bug Finder™, you can check C/C++ code for defects and coding standard violations.
Using Polyspace Code Prover™, you can prove the absence of certain types of run-time errors in C/C++ code.

For more information, see Run Static Analysis in Polyspace Platform User Interface.

You can customize the options used to run a Polyspace Bug Finder or Polyspace Code Prover analysis. This topic lists Code Prover analysis options that are available in the Polyspace Platform user interface.

To configure options, double-click the Configuration node of a Polyspace Platform project. On the Configuration pane, the Code Prover analysis options are distributed over two tabs:

Project — This tab contains project-wide options that are relevant to both static analysis and dynamic testing using Polyspace products. See Project.
Build — This tab contains options that are applicable to both static analysis and dynamic testing using Polyspace products. See Build.
Static Analysis — This tab contains options that are applicable to the static analysis products, Bug Finder and Code Prover. The Run Time Errors node and the nodes below contain options that are specific to a Code Prover analysis. See Static Analysis.

Project

This table shows the options in the Project tab that are relevant to Polyspace Code Prover analysis:

Option	Description	More Information
Name	See name of Polyspace Platform project.	See `Name`.
Author	Specify author name for Polyspace Platform project.	See `Author`.
Created	See date and time when Polyspace Platform project was created.	See `Created`.
Last modified	See date and time when Polyspace Platform project was last modified.	See `Last modified`.
Source code encoding	Specify the encoding of your source files.	See `Source code encoding (-sources-encoding)`
Application source files	Add source files to Polyspace Platform project.	See `Application source files`.
Application source folders	Add source folders to Polyspace Platform project.	See `Application source folders`.
Include paths	Specify paths to folders containing include files.	See `Include paths (-I)`.
Include file name patterns	Specify patterns for file names to be included in Polyspace Platform project.	See `Include file name patterns`.
Exclude paths	Specify folders or files to be excluded from static analysis.	See `Exclude paths`.
Project variables	Define environment variables for use as shorthands in Polyspace Platform project.	See `Project variables`.

Build

The Target & Compiler node on the General tab is equivalent to the Target & Compiler node in a standard Polyspace configuration (that is, one created in the standard Polyspace user interface), with some minor differences. For more information on the differences, see Differences in Configuration Options Between Polyspace Projects and Polyspace Platform Projects.

Target & Compiler

The options on the Target & Compiler node are listed below.

Option	Description	More Information
Source code language	Specify language of source files	See `Source code language (-lang)`.
C standard version	Specify C language standard followed in source code	See `C standard version (-c-version)`.
C++ standard version	Specify C++ language standard followed in source code	See `C++ standard version (-cpp-version)`.
Processor	Select the processor for the current build configuration	See `Processor`.
Compilation toolchain (Static analysis)	Specify the compiler that you use to build your source code. The option applies to static analysis only. To specify a compilation toolchain for testing, specify the option 'Compilation toolchain (Testing)'	See `Compilation toolchain (Static Analysis)`.
Round down results of negative integer division	Specify that your compiler rounds down a negative quotient from dividing two integers	See `Round down results of negative integer division (-div-round-down)`.
Pack alignment value	Specify default structure packing alignment for code developed in Visual C++^®	See `Pack alignment value (-pack-alignment-value)`.
Shift right on signed integers as arithmetic shift	Specify that your compiler implements right shifts on signed integers as arithmetic shifts	See `Shift right on signed integers as arithmetic shift (-logical-signed-right-shift)`.
Preprocessor definitions	Replace macros in preprocessed code	See `Preprocessor definitions (-D)`.
Disabled preprocessor definitions	Undefine macros in preprocessed code	See `Disabled preprocessor definitions (-U)`.
Forced includes	Specify files to be #include-d by every source file	See `Forced includes (-include)`.
Additional include paths	Specify build-specific include paths in addition to project-wide include paths	See `Additional include paths (-I)`.

In projects created from a build command, you also see these additional read-only options:

Static Analysis

The nodes on the Static Analysis tab are equivalent to the nodes with the same name in a standard Polyspace configuration (that is, one created in the standard Polyspace user interface), with some minor differences. For more information on the differences, see Differences in Configuration Options Between Polyspace Projects and Polyspace Platform Projects.

Environment Settings

The options on the Environment Settings node are listed below.

Option	Description	More Information
Stop analysis if a file does not compile	Specify that a compilation error must stop the analysis	See `Stop analysis if a file does not compile (-stop-if-compile-error)`.
Command/script to apply to preprocessed files	Specify command or script to run on source files after preprocessing phase of analysis	See `Command/script to apply to preprocessed files (-post-preprocessing-command)`.
Code from DOS or Windows file system	Consider that file paths are in MS-DOS style	See `Code from DOS or Windows file system (-dos)`.

Inputs & Stubbing

The options on the Inputs & Stubbing node are listed below.

Option	Description	More Information
Constraint setup	Constrain global variables, function inputs and return values of stubbed functions	See `Constraint setup (-data-range-specifications)`.
Ignore default initialization of global variables	Consider global variables as uninitialized unless explicitly initialized in code	See `Ignore default initialization of global variables (-no-def-init-glob)`.
Functions to stub	Specify functions to stub during analysis	See `Functions to stub (-functions-to-stub)`.
Libraries used	Specify libraries that you use in your program	See `Libraries used (-library)`.

Multitasking

The options on the Multitasking node are listed below.

Option	Description	More Information
Enable automatic concurrency detection for Code Prover	Automatically detect certain families of multithreading functions	See `Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection)`.
Specify multitasking configuration	Specify if you want to setup multitasking configuration by using an external file.	See `Specify multitasking configuration using file`.
External multitasking configuration	Specify which supported external file format you want to use to set up your multitasking configuration.	See `External file for multitasking`.
Configure multitasking manually	Consider that code is intended for multitasking	See `Configure multitasking manually`.
Tasks	Specify functions that serve as tasks to your multitasking application	See `Tasks (-entry-points)`.
Cyclic tasks	Specify functions that represent cyclic tasks	See `Cyclic tasks (-cyclic-tasks)`.
Interrupts	Specify functions that represent nonpreemptable interrupts	See `Interrupts (-interrupts)`.
Critical section details	Specify functions that begin and end critical sections	See `Critical section details (-critical-section-begin -critical-section-end)`.
Temporally exclusive tasks	Specify entry point functions that cannot execute concurrently	See `Temporally exclusive tasks (-temporal-exclusions-file)`.

Run Time Errors

The options on the Run Time Errors node are listed below.

Option	Description	More Information
Verify whole application	Stop verification if sources files are incomplete and do not contain a `main` function	See `Verify whole application`.
Show global variable sharing and usage only	Compute global variable sharing and usage without running full analysis	See `Show global variable sharing and usage only (-shared-variables-mode)`.
Verify initialization section of code only	Check initialization code alone for run-time errors and other issues	See `Verify initialization section of code only (-init-only-mode)`.
Verify module or library	Generate a `main` function if source files are modules or libraries that do not contain a `main`	See `Verify module or library (-main-generator)`.
Class	Specify classes that you want to verify	See `Class (-class-analyzer)`.
Functions to call within the specified classes	Specify class methods that you want to verify	See `Functions to call within the specified classes (-class-analyzer-calls)`.
Analyze class contents only	Do not analyze code other than class method	See `Analyze class contents only (-class-only)`.
Skip member initialization check	Do not check if class constructor initializes class members	See `Skip member initialization check (-no-constructors-init-check)`.
Variables to initialize	Specify global variables that you want the generated `main` to initialize	see `Variables to initialize (-main-generator-writes-variables)`.
Initialization functions	Specify functions that you want the generated `main` to call ahead of other functions	See `Initialization functions (-functions-called-before-main)`.
Functions to call	Specify functions that you want the generated `main` to call after the initialization functions	See `Functions to call (-main-generator-calls)`.

Verification Assumption

The options on the Verification Assumption node are listed below.

Option	Description	More Information
Float rounding mode	Specify rounding modes to consider when determining the results of floating point arithmetic	See `Float rounding mode (-float-rounding-mode)`.
Consider volatile qualifier on fields	Assume that `volatile` qualified structure fields can have all possible values at any point in code	See `Consider volatile qualifier on fields (-consider-volatile-qualifier-on-fields)`.
Consider environment pointers as unsafe	Specify that environment pointers can be unsafe to dereference unless constrained otherwise	See `Consider environment pointers as unsafe (-stubbed-pointers-are-unsafe)`.
Ignore assembly code	Specify that assembly instructions in C/C++ code cannot modify C/C++ variables	See `Ignore assembly code (-ignore-assembly-code)`.

Check Behavior

The options on the Check Behavior node are listed below.

Option	Description	More Information
Allow negative operand for left shifts	Allow left shift operations on a negative number	See `Allow negative operand for left shifts (-allow-negative-operand-in-shift)`.
Overflow mode for signed integer	Specify whether result of overflow is wrapped around or truncated	See `Overflow mode for signed integer (-signed-integer-overflows)`.
Overflow mode for unsigned integer	Specify whether result of overflow is wrapped around or truncated	See `Overflow mode for unsigned integer (-unsigned-integer-overflows)`.
Consider non finite floats	Enable an analysis mode that incorporates infinities and NaNs	See `Consider non finite floats (-allow-non-finite-floats)`.
Infinities	Specify how to handle floating-point operations that result in infinity	See `Infinities (-check-infinite)`.
NaNs	Specify how to handle floating-point operations that result in NaN	See `NaNs (-check-nan)`.
Subnormal detection mode	Detect operations that result in subnormal floating-point values	See `Subnormal detection mode (-check-subnormal)`.
Disable checks for non-initialization	Disable checks for non-initialized variables and pointers	See `Disable checks for non-initialization (-disable-initialization-checks)`.
Detect stack pointer dereference outside scope	Find cases where a function returns a pointer to one of its local variables	See `Detect stack pointer dereference outside scope (-detect-pointer-escape)`.
Allow incomplete or partial allocation of structures	Allow a pointer with insufficient memory buffer to point to a structure	See `Allow incomplete or partial allocation of structures (-size-in-bytes)`.
Detect uncalled functions	Detect functions that are not called directly or indirectly from `main` or another entry point function	See `Detect uncalled functions (-uncalled-function-checks)`.
Enable impact analysis	Check for presence or absence of impact between program elements designated as sources and sinks	See `Enable impact analysis (-impact-analysis)`.
Specify sources and sinks	Specify XML file that identifies program elements as sources and sinks for impact analysis	See `Specify sources and sinks (-impact-specifications)`.
Show impact analysis results only	Skip regular Code Prover checks for run-time errors and perform impact analysis only	See `Show impact analysis results only (-impact-analysis-only)`.
Calculate stack usage	Compute and display the estimates of stack usage	See `Calculate stack usage (-stack-usage)`.

Precision

The options on the Precision node are listed below.

Option	Description	More Information
Precision level	Specify a precision level for the verification	See `Precision level (-O0 \| -O1 \| -O2 \| -O3)`.
Verification level	Specify number of times the verification process runs on your code	See `Verification level (-to)`.
Sensitivity context	Store call context information to identify function call that caused errors	See `Sensitivity context (-context-sensitivity)`.
Improve precision of interprocedural analysis	Avoid certain verification approximations for code with fewer lines	See `Improve precision of interprocedural analysis (-path-sensitivity-delta)`.
Specific precision	Specify source files you want to verify at higher precision than the remaining verification	See `Specific precision (-modules-precision)`.

Scaling

The options on the Scaling node are listed below.

Option	Description	More Information
Inline	Specify functions that must be cloned internally for each function call	See `Inline (-inline)`.
Set depth of verification inside structures	Specify that depth of verification inside structures must be specified	See `Set depth of verification inside structures`.
Depth of verification inside structures	Limit the depth of analysis for nested structures	See `Depth of verification inside structures (-k-limiting)`.

Reporting

The options on the Reporting node are listed below.

Option	Description	More Information
Generate report	Specify whether to generate a report after the analysis	See `Generate report`.
Report template (Code Prover)	Specify template for generating analysis report	See `Report template (Code Prover or Bug Finder)`.
Output format	Specify output format of generated report	See `Output format (-report-output-format)`.

Computing Settings

The options on the Computing Settings node are listed below.

Option	Description	More Information
Verification time limit	Specify a time limit on your verification	See `Verification time limit (-timeout)`.

Advanced

The options on the Advanced node are listed below.

Option	Description	More Information
Command/script to apply after the end of the code verification	Specify a time limit on your verification	See `Command/script to apply after the end of the code verification (-post-analysis-command)`.
Other	Specify additional flags for analysis	See `Other`.