主要内容

跑步波尔盖斯代码箴言在服务器上并将结果上传到Web界面

波尔盖斯®代码PROVER™SERVER™证明了C / C ++代码中没有运行时错误，然后将查询上传到Web界面以进行代码审查。

您可以将代码先报运行作为持续集成的一部分。设置以规则的间隔或基于新的代码提交运行代码抄本分析的脚本。脚本可以上传分析结果，以便在PolySpace Web界面中进行审查，并可选择将电子邮件发送给带有PolySpace Condings的源文件的所有者。业主可以打开Web界面，以便仅从提交中查看新发现，然后修复或证明问题。

在典型的项目或团队中，PolySpace代码纤维服务器在一些测试服务器上定期运行并上传结果进行审核。团队中的每个开发商和优质工程师都有一个PolySpace Code Prover Access™许可证在Web界面中查看结果进行调查和错误修复。

先决条件

在服务器上运行代码抄本分析并查看结果PolySpace代码抄本访问Web界面，执行此一次性设置：

  • 要运行分析，请安装一个实例PolySpace代码纤维服务器产品。

  • 要上传结果，请设置托管Web界面所需的组件PolySpace代码抄本访问．

  • 要查看上传的结果，您和每个审查结果的开发人员必须有一个PolySpace代码抄本访问执照。

看安装PolySpace服务器和访问产品下载188bet金宝搏．

查看波尔盖斯安装

检查if.PolySpace代码纤维服务器已安装：

  1. 打开命令窗口。导航polyspaceerverroot.\ polyspace \ bin．这里，polyspaceerverroot.是PolySpace代码纤维服务器例如，安装文件夹，C：\ Program Files \ PolySpace Server \R2021A．也可以看看安装文件夹．

  2. 进入：

    PolySpace-Code-Prover-server -help

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

要检查Polyspace的web界面是否设置为上传:

  1. 再次导航到polyspaceerverroot.\ polyspace \ bin．

  2. 进入：

    PolySpace-Access -Host HostName -port PortNumber -Create-Project TestProject

    这里，主机名是托管服务器的名称PolySpace代码抄本访问网络服务器。对于本地托管的服务器，使用localhost.．Portnumber.我是服务器的可选端口号。如果您省略了端口号，9443.用来。

    如果设置完成，则一个项目调用testproject.是在PolySpace Web界面中创建的。

    每次使用时都会提示您输入您的登录名和密码polyspace-access命令。为避免每次输入登录信息，请使用该命令提供密码的登录名和加密版本。要创建加密密码，请输入：

    PolySpace-Access -encrypt-password

    输入您的登录名和密码。复制加密密码并提供此加密密码-encrypted密码选项使用时polyspace-access命令。

  3. 在网络浏览器中，打开这个URL:

    https：//主机名：Portnumber./metrics/index.html.
    这里，主机名和Portnumber.是上一步的主机名和端口号。

在里面项目资源管理器Pane在PolySpace Web界面上，您应该看到新创建的项目testproject.．

在示例文件上运行代码抄本

要在操作系统中运行代码抄本，请打开命令窗口。

  1. 要运行代码抄本分析，请使用PolySpace-Code-Prover-Server命令。

  2. 要将结果上传到PolySpace Web界面，请使用polyspace-access命令。

为避免键入命令的完整路径，请添加路径polyspaceerverroot.\ polyspace \ bin到了小路操作系统上的环境变量。

尝试使用PolySpace安装提供的样本文件的命令。

  1. 复制示例源文件polyspaceerverroot.\ polyspace \ examples \ cxx \ code_prover_example \源到另一个文件夹，您可以在其中写入权限。在命令行导航到此文件夹。

  2. 进入：

    polyspace-code-prover-server -sources example.c,single_file_analysis.c -I。主发电机-results-dir。polyspace-access主机主机名-港口Portnumber.-登录用户名-encrypted密码PWD-Create-Project TestProject PolySpace-Access -Host主机名-港口Portnumber.-登录用户名-encrypted密码PWD- 加载。-project myfirstproject -parent-project testproject

    这里，用户名您的登录名是和PWD是您之前创建的加密密码。看检查PolySpace安装．

刷新Polyspace网页界面。你可以看到新上传的结果testproject.文件夹在项目资源管理器窗格。

要查看项目中的结果，请单击审查．有关更多信息，请参阅PolySpace代码抄本访问文档．也可以使用PolySpace访问界面右上角的按钮。

使用的选项PolySpace-Code-Prover-Server命令是：

  • - 资源：指定逗号分隔的源文件。

  • -一世：指定包含文件夹的路径。使用-一世每次要添加单独的包含文件夹时，标志

  • -results-dir.：指定文件夹的路径PolySpace代码箴言结果将保存。

    请注意，结果文件夹在每个运行时清除并重新填充。为避免在清理期间意外删除文件，而不是使用包含其他文件的现有文件夹，指定PolySpace结果的专用文件夹。

  • 验证模块或库（-Main-Generator）：指定一个主要的如果未在源文件中找到，必须生成函数

有关代码抄本分析的全部选项列表，请参阅PolySpace代码Prover Server中的分析选项．要在帮助浏览器中打开代码抄本文档，请输入：

PolySpace-Code-Prover-server -doc

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

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

示例窗口®批处理文件如下所示。在此，在脚本中指定了PolySpace安装的路径。要使用此脚本，请更换polyspaceerverroot.使用您安装的路径。您必须已经生成了用于脚本的加密密码。看检查PolySpace安装．

echo off set polyspace_path = polyspaceerverroot \ polyspace \ bin set login = -host hostname -port portnumber -login用户名-encrypted密码PWD“％polyspace_path％\ polyspace-code-prover-server” -  outsources example.c，single_file_analysis.c -i。^ -main-generator-croesults-dir。“％polyspace_path％\ polyspace-access”％login％-create-project testproject“％polyspace_path％\ polyspace-access”％login％-upload。-project myfirstproject -parent-project testproject暂停

Linux样本®shell脚本如下所示。

polyspace_path = polyspaceerverroot / polyspace / bin login = -host hostname -port portnumber -login用户名-encrypted密码PWD${polyspace-code-prover-server -sources example.c,single_file_analysis.c -I .\ -main-generator -result -dir .ctestProject ${POLYSPACE_PATH}/polyspace-access $LOGIN -upload。-project myfirstproject -parent-project testproject

从启动脚本中指定单独的文件中的源和选项

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

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

考虑前面示例中的脚本。你可以修改PolySpace-Code-Prover-Server命令使用带有源和选项的文本文件。而不是:

polyspace-code-prover-server -sources example.c,single_file_analysis.c -I。主发电机-results-dir。

用：

PolySpace-Code-Prover-server -sources列表文件sources.txt -options-file polyspace_opts.txt -Results-Dir。

这里：

  • sources.txt.列出源文件：

    example.c single_file_analysis.c.

  • polyspace_opts.txt.在单独的行中列出分析选项：

    -一世 。-Main-ungener

通常，您的源文件是在构建命令（makefile）中指定的。您可以跟踪Build命令以创建源规范列表的构建命令而不是直接指定源文件。看PolySpace配置（PolySpace代码箴言）．

完成工作流程

在典型的持续积分工作流程中，您运行一个执行这些步骤的脚本：

  1. 从Build命令中提取PolySpace选项。

    例如，如果使用makefiles构建源代码，则可以从Makefile中提取分析选项。

    polyspace-configure -output-options-file compile_opts make

    也可以看看：

  2. 使用先前创建的选项文件运行分析。附加第二个选项文件，该文件包含分析所需的剩余选项。

    polyspace-code-prover-server -options-file compile_opts -options-file run_opts

    看准备PolySpace分析的脚本．

  3. 将结果上传到PolySpace代码抄本访问．

    polyspace-access登录- 加载resultsFolder-项目projName- 议题项目parentprojname.

    这里，登录是与托管的Web服务器通信所需的选项的组合PolySpace代码抄本访问：

    主机主机名-港口Portnumber.-登录用户名-encrypted密码PWD

    resultsFolder是包含Polyspace结果的文件夹。projName和parentprojname.是项目和父文件夹的名称，因为它们会出现在PolySpace代码抄本访问Web界面。

  4. （可选）将电子邮件通知向开发人员发送，其中包含其代码提交的新结果。该电子邮件包含带有结果的链接的附件PolySpace代码抄本访问Web界面。

    看通过PolySpace代码纤维服务器服务器发送电子邮件通知．

请参阅执行以下步骤的脚本示例Jenkins的PolySpace分析示例脚本．

也可以看看

|

相关的话题

PolySpace Code Prover Server文档

金宝app

尝试matlab，sim金宝appulink等产品下载188bet金宝搏

立即获得审判