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

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)` (Polyspace Code Prover).
C standard version	Specify C language standard followed in source code	See `C standard version (-c-version)` (Polyspace Code Prover).
C++ standard version	Specify C++ language standard followed in source code	See `C++ standard version (-cpp-version)` (Polyspace Code Prover).
Processor	Select the processor for the current build configuration	See `Processor` (Polyspace Code Prover).
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)` (Polyspace Code Prover).
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)` (Polyspace Code Prover).
Pack alignment value	Specify default structure packing alignment for code developed in Visual C++^®	See `Pack alignment value (-pack-alignment-value)` (Polyspace Code Prover).
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)` (Polyspace Code Prover).
Preprocessor definitions	Replace macros in preprocessed code	See `Preprocessor definitions (-D)` (Polyspace Code Prover).
Disabled preprocessor definitions	Undefine macros in preprocessed code	See `Disabled preprocessor definitions (-U)` (Polyspace Code Prover).
Forced includes	Specify files to be #include-d by every source file	See `Forced includes (-include)` (Polyspace Code Prover).
Additional include paths	Specify build-specific include paths in addition to project-wide include paths	See `Additional include paths (-I)` (Polyspace Code Prover).

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

Implicit C(C++) compiler include paths (Polyspace Code Prover)
Implicit C(C++) compiler defines (Polyspace Code Prover)

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)` (Polyspace Code Prover).
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)` (Polyspace Code Prover).
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)` (Polyspace Code Prover).

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)` (Polyspace Code Prover).
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)` (Polyspace Code Prover).
Functions to stub	Specify functions to stub during analysis	See `Functions to stub (-functions-to-stub)` (Polyspace Code Prover).
Libraries used	Specify libraries that you use in your program	See `Libraries used (-library)` (Polyspace Code Prover).

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)` (Polyspace Code Prover).
Specify multitasking configuration	Specify if you want to setup multitasking configuration by using an external file.	See `Specify multitasking configuration using file` (Polyspace Code Prover).
External multitasking configuration	Specify which supported external file format you want to use to set up your multitasking configuration.	See `External file for multitasking` (Polyspace Code Prover).
Configure multitasking manually	Consider that code is intended for multitasking	See `Configure multitasking manually` (Polyspace Code Prover).
Tasks	Specify functions that serve as tasks to your multitasking application	See `Tasks (-entry-points)` (Polyspace Code Prover).
Cyclic tasks	Specify functions that represent cyclic tasks	See `Cyclic tasks (-cyclic-tasks)` (Polyspace Code Prover).
Interrupts	Specify functions that represent nonpreemptable interrupts	See `Interrupts (-interrupts)` (Polyspace Code Prover).
Critical section details	Specify functions that begin and end critical sections	See `Critical section details (-critical-section-begin -critical-section-end)` (Polyspace Code Prover).
Temporally exclusive tasks	Specify entry point functions that cannot execute concurrently	See `Temporally exclusive tasks (-temporal-exclusions-file)` (Polyspace Code Prover).

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` (Polyspace Code Prover).
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)` (Polyspace Code Prover).
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)` (Polyspace Code Prover).
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)` (Polyspace Code Prover).
Class	Specify classes that you want to verify	See `Class (-class-analyzer)` (Polyspace Code Prover).
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)` (Polyspace Code Prover).
Analyze class contents only	Do not analyze code other than class method	See `Analyze class contents only (-class-only)` (Polyspace Code Prover).
Skip member initialization check	Do not check if class constructor initializes class members	See `Skip member initialization check (-no-constructors-init-check)` (Polyspace Code Prover).
Variables to initialize	Specify global variables that you want the generated `main` to initialize	see `Variables to initialize (-main-generator-writes-variables)` (Polyspace Code Prover).
Initialization functions	Specify functions that you want the generated `main` to call ahead of other functions	See `Initialization functions (-functions-called-before-main)` (Polyspace Code Prover).
Functions to call	Specify functions that you want the generated `main` to call after the initialization functions	See `Functions to call (-main-generator-calls)` (Polyspace Code Prover).

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)` (Polyspace Code Prover).
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)` (Polyspace Code Prover).
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)` (Polyspace Code Prover).
Ignore assembly code	Specify that assembly instructions in C/C++ code cannot modify C/C++ variables	See `Ignore assembly code (-ignore-assembly-code)` (Polyspace Code Prover).

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)` (Polyspace Code Prover).
Overflow mode for signed integer	Specify whether result of overflow is wrapped around or truncated	See `Overflow mode for signed integer (-signed-integer-overflows)` (Polyspace Code Prover).
Overflow mode for unsigned integer	Specify whether result of overflow is wrapped around or truncated	See `Overflow mode for unsigned integer (-unsigned-integer-overflows)` (Polyspace Code Prover).
Consider non finite floats	Enable an analysis mode that incorporates infinities and NaNs	See `Consider non finite floats (-allow-non-finite-floats)` (Polyspace Code Prover).
Infinities	Specify how to handle floating-point operations that result in infinity	See `Infinities (-check-infinite)` (Polyspace Code Prover).
NaNs	Specify how to handle floating-point operations that result in NaN	See `NaNs (-check-nan)` (Polyspace Code Prover).
Subnormal detection mode	Detect operations that result in subnormal floating-point values	See `Subnormal detection mode (-check-subnormal)` (Polyspace Code Prover).
Disable checks for non-initialization	Disable checks for non-initialized variables and pointers	See `Disable checks for non-initialization (-disable-initialization-checks)` (Polyspace Code Prover).
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)` (Polyspace Code Prover).
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)` (Polyspace Code Prover).
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)` (Polyspace Code Prover).
Enable impact analysis	Check for presence or absence of impact between program elements designated as sources and sinks	See `Enable impact analysis (-impact-analysis)` (Polyspace Code Prover).
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)` (Polyspace Code Prover).
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)` (Polyspace Code Prover).
Calculate stack usage	Compute and display the estimates of stack usage	See `Calculate stack usage (-stack-usage)` (Polyspace Code Prover).

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)` (Polyspace Code Prover).
Verification level	Specify number of times the verification process runs on your code	See `Verification level (-to)` (Polyspace Code Prover).
Sensitivity context	Store call context information to identify function call that caused errors	See `Sensitivity context (-context-sensitivity)` (Polyspace Code Prover).
Improve precision of interprocedural analysis	Avoid certain verification approximations for code with fewer lines	See `Improve precision of interprocedural analysis (-path-sensitivity-delta)` (Polyspace Code Prover).
Specific precision	Specify source files you want to verify at higher precision than the remaining verification	See `Specific precision (-modules-precision)` (Polyspace Code Prover).

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)` (Polyspace Code Prover).
Set depth of verification inside structures	Specify that depth of verification inside structures must be specified	See `Set depth of verification inside structures` (Polyspace Code Prover).
Depth of verification inside structures	Limit the depth of analysis for nested structures	See `Depth of verification inside structures (-k-limiting)` (Polyspace Code Prover).

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` (Polyspace Code Prover).
Report template (Code Prover)	Specify template for generating analysis report	See `Report template (Code Prover or Bug Finder)` (Polyspace Code Prover).
Output format	Specify output format of generated report	See `Output format (-report-output-format)` (Polyspace Code Prover).

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)` (Polyspace Code Prover).

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)` (Polyspace Code Prover).
Other	Specify additional flags for analysis	See `Other` (Polyspace Code Prover).