本页翻译不是最新的。点击此处可查看最新英文版本。

polyspace-code-prover

(DOS/UNIX) 从 Windows、Linux 或其他命令行运行 Code Prover 验证

全页折叠

语法

polyspace-code-prover [options]
polyspace-code-prover -sources sourceFiles [options]
polyspace-code-prover -sources-list-file listOfSources [options]
polyspace-code-prover -options-file optFile
polyspace-code-prover -h[elp]

说明

注意

此 Polyspace® 命令在 polyspaceroot\polyspace\bin 中可用。其中，polyspaceroot 是 Polyspace 的安装文件夹，例如 C:\Program Files\Polyspace\R2024b（另请参阅安装文件夹）。为避免键入此命令的完整路径，请将此位置添加到操作系统中的 PATH 环境变量中。

如果当前文件夹包含具有源文件（.c 或 .cxx 文件）的 sources 子文件夹，则 polyspace-code-prover [options] 会运行 Code Prover 验证。验证操作会考虑位于 sources 以及 sources 下的所有子文件夹中的文件。您可以使用附加选项来自定义验证。

polyspace-code-prover -sources sourceFiles [options] 对源文件 sourceFiles 运行 Code Prover 验证。您可以使用附加选项来自定义验证。

示例

polyspace-code-prover -sources-list-file listOfSources [options] 对 listOfSources 文本文件中列出的源文件运行 Code Prover 验证。您可以使用附加选项来自定义验证。

polyspace-code-prover -options-file optFile 使用选项文件中指定的选项运行 Code Prover 验证。

示例

polyspace-code-prover -h[elp] 列出可能的分析选项的汇总。

示例

全部折叠

通过在命令本身中指定分析选项来运行本地 Code Prover 验证。此示例使用了来自 Polyspace Code Prover 演示示例的源文件。要运行此示例，请将 polyspaceroot 替换为您的 Polyspace 安装路径，例如 C:\Program Files\Polyspace\R2024b。

使用 GNU 4.7 编译器设置对 numerical.c 和 programming.c 运行验证，检查 MISRA C:2012 强制规则。为方便阅读，我们使用 ^ 字符对此示例命令进行了拆分。实际上，您可以将所有命令放在一行中。

polyspace-code-prover -lang C^
 -sources polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\*.c,^
 -I polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\^
 -compiler generic -misra3 mandatory^
 -author jlittle -prog myProject -results-dir C:\Polyspace_Workspace\Results\

打开结果。

polyspace C:\Polyspace_Workspace\Results\ps_results.pscp

要重新运行验证，您必须从命令行重新运行该验证。

通过使用选项文件指定源文件和分析选项来运行验证。要运行此示例，请将 polyspaceroot 替换为您的 Polyspace 安装路径，例如 C:\Program Files\Polyspace\R2024b。

将以下文本保存到名为 myOptsFile.txt 的文本文件。

# Polyspace analysis options 
-I polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources
-verif-version 1.0
-sources polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\*.c
-lang C
-target i386
-compiler generic
-dos
-do-not-generate-results-for all-headers
-misra3 mandatory-required
-entry-points proc1,proc2,server1,server2,tregulate
-critical-section-begin Begin_CS:Cs10
-critical-section-end End_CS:Cs10
-temporal-exclusions-file polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\temporal_exclusions.txt
-float-rounding-mode to-nearest
-signed-integer-overflows forbid
-unsigned-integer-overflows allow
-uncalled-function-checks none
-check-subnormal allow
-O2
-to Software Safety Analysis level 2
-context-sensitivity-auto
-path-sensitivity-delta 0
-author jlittle 
-prog myProject 
-results-dir C:\Polyspace_Workspace\Results\

使用文本文件中指定的选项运行验证。

polyspace-code-prover -options-file myOptsFile.txt

打开结果。

polyspace C:\Polyspace_Workspace\Results\ps_results.pscp

要重新运行验证，您必须从命令行重新运行该验证。

输入参数

全部折叠

以逗号分隔的 C 或 C++ 源文件名称，指定为字符串。如果文件不在当前文件夹 (pwd) 中，则 sourceFiles 必须包含完整路径或相对路径。为避免因路径带有空格而导致错误，请在路径两端加上引号 " "。有关详细信息，请参阅-sources。

如果当前文件夹包含具有源文件的 sources 子文件夹，则可以省略 -sources 标志。验证操作会考虑位于 sources 以及 sources 下的所有子文件夹中的文件。

示例: myFile.c, "C:\mySources\myFile1.c,C:\mySources\myFile2.c"

列出 C 或 C++ 文件名称的文本文件，指定为字符串。如果文件不在当前文件夹 (pwd) 中，则 listOfSources 必须包含完整路径或相对路径。为避免因路径带有空格而导致错误，请在路径两端加上引号 " "。有关详细信息，请参阅-sources-list-file。

示例: filename.txt, "C:\ps_analysis\source_files.txt"

分析选项及其对应的值，由选项名称和值（如果适用）指定。有关语法规范，请参阅各个分析选项参考页。

示例: -lang C-CPP, -target i386

列出分析选项和值的文本文件，指定为字符串。有关详细信息，请参阅-options-file。

示例: opts.txt, "C:\ps_analysis\options.txt"

提示

如果您将该命令作为脚本的一部分运行，请检查退出状态来确认分析是否成功。该命令在分析成功时将返回零。返回值为非零，则意味着分析失败且未完成。例如，如果分析文件未进行编译，则此命令将返回一个非零值。如果在分析多个文件时某些文件未进行编译，则此命令会完成对进行了编译的文件的分析并返回零。如果文件未编译，可以选择停止分析。请参阅Stop analysis if a file does not compile (-stop-if-compile-error)。

运行此命令后，您可以在 Windows 命令行中检查 %ERRORLEVEL% 变量来确认分析是否成功。

版本历史记录

在 R2013b 中推出

另请参阅

主题