主要内容

Polyspace 平台用户界面中的 Bug Finder 分析

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

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

Polyspace 选项

全部展开

基本信息

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

源文件和包含文件夹

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

文件包含和排除

包括文件名模式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)指定源代码中遵循的 C 语言标准。
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)为在 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)考虑文件路径为 MS-DOS 格式

输入和插桩

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

多任务

使用文件指定多任务配置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
禁用所有中断 (-routine-disable-interrupts -routine-enable-interrupts)Specify routines that disable and reenable 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

缺陷和编码标准

使用自定义检查项文件指定检查项必须使用检查项激活 XML 文件来指定。 (自 R2023b 起)
检查项激活文件 (-checkers-activation-file)激活自定义的缺陷和编码规则组合,以进行 Polyspace Bug Finder 分析 (自 R2021a 起)
使用生成代码的要求 (-misra3-agc-mode)检查是否存在违反适用于生成的代码的 MISRA C:2012 规则和指令的情形
使用生成代码的要求 (-misra-c-2023-agc-mode)检查是否存在违反适用于生成的代码的 MISRA C:2023 规则和指令的情形 (自 R2024a 起)
计算代码度量 (-code-metrics)计算并显示代码复杂度度量
为源代码和以下项生成结果 (-generate-results-for)指定要进行分析的文件。
不为以下项生成结果 (-do-not-generate-results-for)指定不希望进行分析的文件

检查项行为

有效布尔类型 (-boolean-types)Specify data types that coding rule checker must treat as effectively Boolean
允许的 pragma (-allowed-pragmas)Specify pragma directives that are documented
运行更严格的检查并考虑所有的系统输入值 (-checks-using-system-input-values)Enable stricter checks and provide examples of values that lead to detected defect

报告

生成报告指定在分析后是否生成报告
报告模板(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 平台用户界面

文件存储