polyspace-code-prover

（系统命令）从 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-code-prover 系统命令可在命令行使用指定为命令行标志的分析选项或使用选项文件来运行 Polyspace® Code Prover™ 分析。

注意

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

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

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

示例

polyspace-code-prover -sources-list-file listOfSources [options] 对 listOfSources 文本文件中列出的源文件运行 Code Prover 验证。您可以使用附加选项来自定义验证。当您有许多源文件分散在多个文件夹中时，建议使用源文件列表文件。通过将源文件列表保存在文本文件中，您可以控制分析范围，并在不将源文件移动到 sources 文件夹的情况下将源文件添加到分析中。

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

示例

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

示例

全部折叠

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

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

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^
 -author jlittle -prog myProject -results-dir C:\Polyspace_Workspace\Results\

打开结果。

polyspace C:\Polyspace_Workspace\Results\ps_results.pscp

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

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

将以下文本保存到名为 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
-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 必须包含完整路径或相对路径。为避免因路径带有空格而导致错误，请在路径两端加上引号 " "。您还可以使用通配符来分析特定文件夹中所有扩展名为 .c 或 .cpp 的源文件。有关详细信息，请参阅应用程序源文件 (-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 中推出

另请参阅

|

主题