Main Content

Code Prover Analysis in Polyspace Platform User Interface

Check C/C++ code for defects in the Polyspace® Platform user interface

Polyspace Platform is an integrated environment that supports static analysis and dynamic testing of C/C++ code with Polyspace products. In the Polyspace Platform user interface, you can create a project, add source files, configure analysis options, and run a Code Prover analysis.

Polyspace Options

expand all

Basic Info

NameSee name of Polyspace Platform project (Since R2024a)
AuthorSpecify author name for Polyspace Platform project (Since R2024a)
CreatedSee date and time when Polyspace Platform project was created (Since R2024a)
Last modifiedSee date and time when Polyspace Platform project was last modified (Since R2024a)
Source code encoding (-sources-encoding)Specify the encoding of source files

Sources, Includes, and Tests

Include pathsSpecify paths to folders containing include files (Since R2023b)
Application source foldersAdd source folders to Polyspace Platform project (Since R2024a)
Application source filesAdd source files to Polyspace Platform project (Since R2024a)

File Inclusions and Exclusions

Include file name patternsSpecify patterns for file names to be included in Polyspace Platform project (Since R2024a)
Exclude pathsSpecify folders or files to be excluded from static analysis or testing (Since R2024a)

Environment Variables

Project variablesDefine environment variables for use as shorthands in Polyspace Platform project (Since R2024a)

Target & Compiler

Source code language (-lang)Specify language of source files
C standard version (-c-version)Specify C language standard followed in source code
C++ standard version (-cpp-version)Specify C++ language standard followed in source code
ProcessorSelect the processor for the current build configuration
Compilation toolchain (Static Analysis)Specify the compiler that you use to build your source code for static analysis
Round down results of negative integer division (-div-round-down)Specify that your compiler rounds down a negative quotient from dividing two integers (Since R2023b)
Pack alignment value (-pack-alignment-value)Specify default structure packing alignment for code developed in Visual C++
Shift right on signed integers as arithmetic shift (-logical-signed-right-shift)Specify that your compiler implements right shifts on signed integers as arithmetic shifts (Since R2023b)
Preprocessor definitions (-D)Replace macros in preprocessed code
Disabled preprocessor definitions (-U)Undefine macros in preprocessed code
Forced includes (-include)Specify files to be #include-d by every source file. (Since R2023b)
Additional include paths (-I)Specify build-specific include paths in addition to project-wide include paths (Since R2024a)

Environment Settings

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

Inputs & Stubbing

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

Multitasking

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

Run Time Errors

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

Verification Assumption

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

Check Behavior

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

Precision

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

Scaling

Inline (-inline)Specify functions that must be cloned internally for each function call
Set depth of verification inside structuresSpecify that depth of verification inside structures must be specified (Since R2023b)
Depth of verification inside structures (-k-limiting)Limit the depth of analysis for nested structures

Reporting

Generate reportSpecify whether to generate a report after the analysis
Report template (Code Prover or Bug Finder)Specify template for generating analysis report
Output format (-report-output-format)Specify output format of generated report

Computing Settings

Verification time limit (-timeout)Specify a time limit on your analysis

Advanced

Command/script to apply after the end of the code verification (-post-analysis-command)Specify command or script to be executed after analysis
OtherSpecify additional command-line flags for static analysis

Topics

Getting Started

Create and Update Project

Configure Project

File Storage