在 Polyspace 平台用户界面中进行 Code Prover 分析

在 Polyspace® 平台用户界面中检查 C/C++ 代码中是否存在缺陷

Polyspace 平台是一个集成环境，支持使用 Polyspace 产品对 C/C++ 代码进行静态分析和动态测试。在 Polyspace 平台用户界面中，您可以创建工程、添加源文件、配置分析选项并运行 Code Prover 分析。

Polyspace 选项

全部展开

基本信息

名称See name of Polyspace Platform project (自 R2024a 起)
作者Specify author name for Polyspace Platform project (自 R2024a 起)
创建时间See date and time when Polyspace Platform project was created (自 R2024a 起)
最后修改时间See date and time when Polyspace Platform project was last modified (自 R2024a 起)
源代码编码 (-sources-encoding)指定源文件的编码

源、包含和测试

包含路径指定包含文件所在文件夹的路径 (自 R2023b 起)
应用程序源文件夹Add source folders to Polyspace Platform project (自 R2024a 起)
应用程序源文件Add source files to Polyspace Platform project (自 R2024a 起)

文件包含和排除

包括文件名模式Specify patterns for file names to be included in Polyspace Platform project (自 R2024a 起)
排除路径Specify folders or files to be excluded from static analysis or testing (自 R2024a 起)

环境变量

工程变量Define environment variables for use as shorthands in Polyspace Platform project (自 R2024a 起)

目标和编译器

源代码语言 (-lang)Specify language of source files
C 标准版本 (-c-version)Specify C language standard followed in source code
C++ 标准版本 (-cpp-version)Specify C++ language standard followed in source code
处理器Select the processor for the current build configuration
编译工具链(静态分析)Specify the compiler that you use to build your source code for static analysis
向下舍入负的整数相除结果 (-div-round-down)Specify that your compiler rounds down a negative quotient from dividing two integers (自 R2023b 起)
包对齐值 (-pack-alignment-value)Specify default structure packing alignment for code developed in Visual C++
指定编译器以算术移位方式右移有符号整数 (-logical-signed-right-shift)Specify that your compiler implements right shifts on signed integers as arithmetic shifts (自 R2023b 起)
预处理器定义 (-D)替换预处理代码中的宏
已禁用的预处理器定义 (-U)取消定义预处理代码中的宏
强制包含文件 (-include)Specify files to be #include-d by every source file. (自 R2023b 起)
其他包含路径 (-I)Specify build-specific include paths in addition to project-wide include paths (自 R2024a 起)

环境设置

如果文件无法编译，则停止分析 (-stop-if-compile-error)Specify that a compilation error must stop the analysis
要应用于预处理文件的命令/脚本 (-post-preprocessing-command)Specify command or script to run on source files after preprocessing phase of analysis
代码来自 DOS 或 Windows 文件系统 (-dos)Consider that file paths are in MS-DOS style

输入和插桩

约束设置 (-data-range-specifications)对插桩函数的全局变量、函数输入和返回值进行约束
忽略全局变量的默认初始化 (-no-def-init-glob)Consider global variables as uninitialized unless explicitly initialized in code
要插桩的函数 (-functions-to-stub)Specify functions to stub during analysis
使用的库 (-library)Specify libraries that you use in your program (自 R2021a 起)

多任务

为 Code Prover 启用自动并发检测 (-enable-concurrency-detection)自动检测某些系列的多线程函数
使用文件指定多任务配置Specify if you want to setup multitasking configuration by using an external file. (自 R2023b 起)
用于多任务的外部文件Specify which supported external file format you want to use to set up your multitasking configuration. (自 R2023b 起)
手动配置多任务Consider that code is intended for multitasking
任务 (-entry-points)Specify functions that serve as tasks to your multitasking application
周期任务 (-cyclic-tasks)Specify functions that represent cyclic tasks
中断 (-interrupts)Specify functions that represent nonpreemptable interrupts
临界区详细信息 (-critical-section-begin -critical-section-end)Specify functions that begin and end critical sections
时序互斥任务 (-temporal-exclusions-file)Specify entry point functions that cannot execute concurrently

运行时错误

验证整个应用程序如果源文件不完整且未包含 main 函数，则停止验证
仅显示全局变量共享和使用情况 (-shared-variables-mode)Compute global variable sharing and usage without running full analysis
仅验证初始化代码段 (-init-only-mode)Check initialization code alone for run-time errors and other issues
验证模块或库 (-main-generator)如果源文件是未包含 main 的模块或库，则生成一个 main 函数
类 (-class-analyzer)Specify classes that you want to verify
指定类内要调用的函数 (-class-analyzer-calls)Specify class methods that you want to verify
仅分析类内容 (-class-only)Do not analyze code other than class methods
跳过成员初始化检查 (-no-constructors-init-check)Do not check if class constructor initializes class members
要初始化的变量 (-main-generator-writes-variables)Specify global variables that you want the generated main to initialize
初始化函数 (-functions-called-before-main)Specify functions that you want the generated main to call ahead of other functions
要调用的函数 (-main-generator-calls)Specify functions that you want the generated main to call after the initialization functions

验证假设

浮点数舍入模式 (-float-rounding-mode)Specify rounding modes to consider when determining the results of floating point arithmetic
考虑字段的 volatile 限定符 (-consider-volatile-qualifier-on-fields)Assume that volatile qualified structure fields can have all possible values at any point in code
将环境指针视为不安全 (-stubbed-pointers-are-unsafe)Specify that environment pointers can be unsafe to dereference unless constrained otherwise
忽略汇编代码 (-ignore-assembly-code)Specify that assembly instructions in C/C++ code cannot modify C/C++ variables (自 R2023a 起)

检查行为

允许左移负操作数 (-allow-negative-operand-in-shift)Allow left shift operations on a negative number
有符号整数的溢出模式 (-signed-integer-overflows)Specify whether result of overflow is wrapped around or truncated
无符号整数的溢出模式 (-unsigned-integer-overflows)Specify whether result of overflow is wrapped around or truncated
考虑非有限浮点数 (-allow-non-finite-floats)Enable an analysis mode that incorporates infinities and NaNs
无穷值 (-check-infinite)Specify how to handle floating-point operations that result in infinity
NaN (-check-nan)Specify how to handle floating-point operations that result in NaN
次正规数值检测模式 (-check-subnormal)Detect operations that result in subnormal floating-point values
禁用非初始化检查 (-disable-initialization-checks)Disable checks for non-initialized variables and pointers
检测超出作用域的堆栈指针解引用 (-detect-pointer-escape)Find cases where a function returns a pointer to one of its local variables
允许不完全或部分分配结构体 (-size-in-bytes)Allow a pointer with insufficient memory buffer to point to a structure
检测未调用的函数 (-uncalled-function-checks)Detect functions that are not called directly or indirectly from main or another entry point function
启用影响分析 (-impact-analysis)Check for presence or absence of impact between program elements designated as sources and sinks (自 R2023b 起)
指定源点和汇点(-impact-specifications)Specify XML file that identifies program elements as sources and sinks for impact analysis (自 R2023b 起)
仅显示影响分析结果 (-impact-analysis-only)Skip regular Code Prover checks for run-time errors and perform impact analysis only (自 R2023b 起)
计算堆栈使用情况 (-stack-usage)计算并显示堆栈使用量的估计值 (自 R2022a 起)

精度

精度等级 (-O0 | -O1 | -O2 | -O3)指定用于验证的精度等级
验证等级 (-to)Specify number of times the verification process runs on your code
敏感度上下文 (-context-sensitivity)Store call context information to identify function call that caused errors
提高过程间分析的精度 (-path-sensitivity-delta)Avoid certain verification approximations for code with fewer lines
特定精度 (-modules-precision)Specify source files you want to verify at higher precision than the remaining verification

规模

内联 (-inline)指定必须要为对其的每次调用在内部创建克隆的函数
设置结构体内部的验证深度Specify that depth of verification inside structures must be specified (自 R2023b 起)
结构体内部的验证深度 (-k-limiting)限制对嵌套结构体的分析深度

报告

生成报告指定在分析后是否生成报告
报告模板（Code Prover 或 Bug Finder）Specify template for generating analysis report
输出格式 (-report-output-format)指定生成的报告的输出格式

计算设置

验证时限 (-timeout)Specify a time limit on your analysis

高级

在代码验证结束后要应用的命令/脚本 (-post-analysis-command)Specify command or script to be executed after analysis
其他为静态分析指定附加命令行标志

系统命令

polyspace-project -diff, polyspace-project -merge(System Command) Compare and merge Polyspace Platform projects before submission to source control
polyspace-project -convert-psprj-to-workspace(System Command) Convert Polyspace project file to Polyspace Platform workspace file and project files
polyspace-project -generate-launching-script-for(System Command) Generate files needed to run static analysis on a Polyspace Platform project

主题

快速入门

创建和更新工程

配置工程

Polyspace 平台用户界面

文件存储