先决条件

要在服务器上运行代码验证器分析并查看多空间码验证访问web界面，执行此一次性设置：

看到安装Polyspace服务器和Access产品下载188bet金宝搏。

检查Polyspace安装

检查如果Polyspace代码验证服务器安装:

您应该看到代码验证器分析所允许的选项列表。

检查Polyspace网页界面是否已设置以供上载:

在工程资源管理器在Polyspace web界面上的窗格中，您应该可以看到新创建的项目testProject。

在示例文件上运行代码验证程序

要在您的操作系统中运行代码验证程序，请打开一个命令窗口。

要避免输入命令的完整路径，请添加路径polyspaceserverroot\polyspace\bin到路径操作系统上的环境变量。

在Polyspace安装提供的样例文件上尝试这些命令。

刷新Polyspace web界面。您可以看到新上传的结果testProject文件夹中工程资源管理器窗玻璃

要查看项目中的结果，请单击审查。有关更多信息，请参见Polyspace代码验证程序访问文档。您也可以使用Polyspace访问界面右上角的按钮。

的选项polyspace-code-prover-server命令是：

有关代码验证器分析可用选项的完整列表，请参见Polyspace代码验证服务器的分析选项. 要在帮助浏览器中打开代码验证程序文档，请输入：

polyspace代码验证服务器-doc

服务器上代码验证程序分析的示例脚本

要运行分析，您可以使用脚本，而不是在命令行中输入命令。脚本可以在每次添加或修改源文件时执行。

窗口示例^®批处理文件如下所示。在这里，Polyspace安装的路径在脚本中指定。若要使用此脚本，请替换polyspaceserverroot您的安装路径。您必须已生成用于脚本的加密密码。看见检查Polyspace安装。

echo off set POLYSPACE_PATH=polyspaceserverroot\polyspace\bin set LOGIN=-host hostName -port portNumber -login . log . log . log . log用户名-加密密码pwd"%POLYSPACE_PATH%\polyspace-code-prover-server" -sources example.c,single_file_analysis.c"%POLYSPACE_PATH%\polyspace-access" %LOGIN% -create-project testProject "暂停项目

Linux示例^®Shell脚本如下所示。

POLYSPACE_PATH=polyspaceserverroot/POLYSPACE/bin LOGIN=-主机名-端口号-登录用户名-加密密码pwd${POLYSPACE_PATH}/polyspace-code-prover-server -sources example.c,single_file_analysis.c -I .\ -main-generator -results-dir .c${POLYSPACE_PATH}/polyspace-access $LOGIN -create-project testProject ${POLYSPACE_PATH}/polyspace-access $LOGIN -upload-project myFirstProject -parent-project testProject

在启动脚本的不同文件中指定源和选项

您可以在单独的文本文件中列出它们，而不是在启动脚本中列出源文件和分析选项。

通过从启动脚本中删除源文件和分析选项规范，您可以在提交新代码时根据需要修改这些规范，同时保持启动脚本不变。

考虑前面示例中的脚本。您可以修改polyspace-code-prover-server命令使用带有源和选项的文本文件。而不是:

example.c,single_file_analysis.c主发电机-results-dir。

使用：

polyspace代码验证服务器-源列表文件sources.txt-选项文件polyspace_opts.txt-结果目录。

在这里:

通常，在生成命令（makefile）中指定源文件。您可以跟踪build命令来创建源规范列表，而不是直接指定源文件。看见多空间配置(Polyspace代码验证)。

完整的工作流程

在一个典型的持续集成工作流中，您运行一个执行以下步骤的脚本:

参见中执行这些步骤的脚本示例使用Jenkins进行多空间分析的示例脚本。