主要内容

跑波尔盖斯生成的代码分析金宝app模型

这个示例使用:

你可以运行polyspace®在Simulink生成的代码上金宝app®模型或子系统。

  • Polyspace Bug Finder™检查错误或编码规则违规的代码（例如，Misra C.®：2012规则）。

  • PolySpace Code Prover™全面检查代码是否存在运行时错误。

如果你使用嵌入式编码器®对于代码生成，本教程展示了如何在简单Simulink模型中生成的代码上运行PolySpace。金宝app对于完整的工作流程，请参阅使用嵌入式编码器生成的代码运行PolySpace分析．

先决条件

在从Simulink运行PolySpace之前，必须将您的P金宝appolySpace和Matlab链接®安装。看到将Polyspace与MATLAB和Simulink集成金宝app．

要打开本例中使用的模型，请在MATLAB命令窗口中运行:

openExample ('PolySpace_Code_prover / OpenModelforCodeGenerationAndpolyspaceanalysisexample'）

代码生成和PolySpace分析的开放模型

这个示例使用:

开放模式

打开模型polyspace_controller_demo.用于配置代码生成和PolySpace分析。

生成和分析代码

要开始对模型生成的代码进行Polyspace分析:

  1. 在这一点应用选项卡上,选择PolySpace代码验证者．

  2. 在这一点波尔盖斯标签，找到分析字段和选择代码生成为Top模型从下拉菜单。

  3. 点击画布上的任何地方。的分析代码字段显示模型名称。选择运行分析．

当您单击时，Polyspace检查生成的代码运行分析．如果没有生成的代码，Polyspace首先使用Embedded Coder生成代码，然后开始分析。

等价的MATLAB代码：

load_system（'polyspace_controller_demo'）;slbuild ('polyspace_controller_demo'）;mlopts = pslinkOptions（'polyspace_controller_demo'）;mlopts.resultdir ='\结果'mopts.verificationMode =.'codeprover'；pslinkrun ('polyspace_controller_demo', mlopts);
要用Bug Finder进行分析，请替换codeprover.和错误机器．有关代码的更多信息，请参阅pslinkoptions和Pslinkrun.．

回顾分析结果

分析后，结果显示在Polyspace用户界面中。

如果您运行Bug Finder，则结果包括在生成的代码中检测到的错误。如果您运行代码谚语，则结果由选中包含颜色编码，如下所示：

  • 绿色（经过验证的代码）:对于提供的数据约束，检查不会失败。例如，除法操作不会导致被零除错误。

  • 红色（验证错误）：检查始终为提供的数据约束集失败。例如，分割操作总是导致一个被零除错误。

  • 橙色(可能的错误):该检查指示未经验证的代码，对于所提供的数据约束的某些值可能会失败。例如，除法运算有时会导致被零除错误。

  • 灰色（无法访问的代码）：检查表示无法达到所提供的数据约束的代码操作。

详细审查每个分析结果。例如，在你的代码验证结果:

  1. 在这一点结果清单窗格，选择红色数组索引越界检查。

  2. 在这一点源窗格，将光标放在红色检查，查看其他信息。例如，红色上的工具提示[操作符声明数组大小和数组索引的可能值。的结果细节窗格还提供此信息。

错误发生在手写的C文件中command_strialy_file.c.．C文件位于S函数块中Command_Strategy在减少精度子系统(在模型引用中)相对阈值）.

跟踪错误到模型并修复它们

对于从模型生成的代码，您可以将错误跟踪回模型。这些部分展示了如何将特定的代码抄本结果追溯到模型。

错误1：超出界限数组索引

  1. 在这一点结果清单窗格，选择橙色数组索引越界文件中发生的错误polyspace_controller_demo.c．

  2. 在这一点源窗格，单击链接S4：76在橙色错误上方的评论中。

    / *转型:“< S4 >: 75”*/ /* 过渡：“< S4 >: 76”* /(我)+ +;/* Outport: '/FaultTable' */FaultTable[*我]= 10;

您可以看到，错误是由于状态流程图中的转换而发生的synch_and_asynch_monitoring.．您可以跟踪错误到状态流图的输入变量索引。

你可以避免数组索引越界在几个方面。一种方法是约束输入变量指数用一个饱和块在StateFlow图表之前。

错误2:溢出

  1. 在这一点结果清单窗格，选择橙色溢出错误如下所示。错误出现在文件中polyspace_controller_demo.c．

  2. 在这一点源窗格，查看错误。要将错误跟踪回模型，请单击链接S1 / GAIN.在橙色错误上方的评论中。

    / *获取:' / gain'合并:* import: '/Battery Info' * import: '/Rotation' * Sum:' / sum1'* / gain =（int16_T) (((int16_T) ((in_rotation + in_battery_info) > > 1) * 24576) > > 10);
    你看到错误发生在故障管理子系统内部获得块后和块。

你可以避免溢出在几个方面。一种方法是限制信号的值in_battery_info.这是送入的和块。限制信号:

  1. 双击import块电池信息提供输入信号in_battery_info.到模型。

  2. 在这一点信号的属性标签，更改最大信号的值。

该模型中的错误是由于以下原因之一引起的:

  • 错误的缩放，未知的校准和未经测试的数据范围从一个子系统进入一个算术块。

  • 基于statflow事件的建模和手写查找表函数中的数组操作。

  • 饱和导致生成的代码内意外的数据流。

  • 故障状态流程编程。

一旦确定错误的根本原因，您就可以妥善修改模型以解决问题。

检查编码规则违规

在开始代码分析之前，检查是否违反代码规则:

  1. 在这一点波尔盖斯选项卡上,选择设置．

  2. 在“配置参数”对话框中，选择适当的选项设置从列表。例如,选择项目配置和Misra C 2012 AGC检查．

    建议您运行Bug Finder以检查Misra C：2012规则。在这一点波尔盖斯选项卡上,选择错误发现者．

  3. 点击申请或好吧并重新运行分析。

注释块以证明结果

您可以通过向块添加注释来证明您的结果。在代码分析期间，PolySpace代码先报员读取您的注释并通过致密化填充结果。一旦证明了结果，您就不必再次审核。

  1. 在这一点结果清单窗格，从左上角的下拉列表中，选择文件．

  2. 在文件中polyspace_controller_demo.c，在功能中polyspace_controller_demo_step（），选择违反MISRA C:2012规则10.4。的源窗格显示添加操作违反规则。

  3. 在这一点源窗格，单击链接S1 / Sum1在上面的注释中添加操作。

    / *获取:' / gain'合并:* import: '/Battery Info' * import: '/Rotation' * Sum:' / sum1'* / gain =（int16_t）（（（int16_t）（（in_rootation + in_battery_info）>> 1）* 24576）>> 10）;

    您可以看到规则违规发生在SUM块中。

    注释此块并证明违反规则:

    1. 选择块。在这一点波尔盖斯选项卡上,选择添加注释．

    2. 选择misra - c - 2012为了注释类型并输入有关规则违规的信息。设定地位到没有计划行动和严重程度到设置．

    3. 点击申请或好吧．这些话PolySpace注释出现在代码块下面，表示该代码块包含代码注释。

    4. 重新生成代码并重新运行分析。的严重程度和地位列在结果清单窗格中预先填充了您的注释。

相关的话题

Polyspace代码验证器文档

金宝app

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

得到审判现在