运行Polyspace分析的代码生成的Simulink模型- MATLAB和Simulink万博1manbetx

运行Polyspace对生成的代码进行分析万博1manbetx模型

这个示例使用:

你可以运行Polyspace^®从Simulink生成的代码万博1manbetx^®模型或子系统。

Polyspace错误发现者™检查代码是否有错误或违反了编码规则(例如，MISRA C^®:2012条规则)。
Polyspace代码验证™详尽地检查代码的运行时错误。

如果你使用嵌入式编码器^®对于代码生成，本教程展示如何在简单的Simulink模型生成的代码上运行Polyspace。万博1manbetx完整的工作流程见对使用嵌入式编码器生成的代码运行Polyspace分析.

先决条件

在从Simulink运行Polyspace之前，必须链接Po万博1manbetxlyspace和MATLAB^®安装。看到将Polyspace与MATLAB和Simulink集成万博1manbetx.

若要打开本例中使用的模型，请在MATLAB帮助浏览器中查找本例并单击开放模式按钮。

开放模型的代码生成和多空间分析

这个示例使用:

开放模式

打开模型polyspace_controller_demo用于配置代码生成和多空间分析。

生成代码

上从模型生成代码应用程序选项卡上,选择嵌入式编码器.在C代码选项卡上,选择生成代码.

等价的MATLAB代码:

load_system (“polyspace_controller_demo”);rtwbuild (“polyspace_controller_demo”);

分析代码

来分析从模型生成的代码应用程序选项卡上,选择Polyspace代码验证器.在Polyspace标签:

选择要运行的产品:错误发现者或代码验证.
单击画布上的任何地方。的分析代码字段显示模型名称。选择运行分析.

等价的MATLAB代码:

mlopts = pslinkoptions (“polyspace_controller_demo”);mlopts。ResultDir =“\结果”mlopts。VerificationMode =“CodeProver”;pslinkrun (“polyspace_controller_demo”,mlopts);

要使用Bug查找程序进行分析，请使用replaceCodeProver与BugFinder.有关代码的更多信息，请参见pslinkoptions和pslinkrun.

回顾分析结果

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

如果您运行Bug Finder，结果将包含在生成的代码中检测到的Bug。如果你运行代码验证器，结果包括检查，颜色编码如下:

绿色(证明代码):对于提供的数据约束，检查不会失败。例如，除法运算不会导致a除零错误。
红色(验证错误):对于提供的一组数据约束，检查总是失败。例如，除法运算总是导致a除零错误。
橙色(可能的错误):该检查指示未经验证的代码，对于提供的数据约束的某些值可能会失败。例如，除法运算有时会导致a除零错误。
灰色(不可到达的代码):该检查指示无法访问所提供的数据约束的代码操作。

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

在结果列表窗格，选择红色越界数组索引检查。
在源窗格中，将光标放在红色复选框上以查看其他信息。例如，工具提示是红色的(运算符声明数组大小和数组索引的可能值。的结果细节窗格还提供此信息。

错误发生在一个手写的C文件中Command_strategy_file.c.C文件在s函数块中Command_Strategy在降低了精度子系统(在模型引用中相对阈值)。

跟踪错误并修复它们

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

错误1:数组索引越界

在结果列表窗格，选择橙色越界数组索引文件中发生的错误polyspace_controller_demo.c.

在源窗格，单击链接S4:76在评论上面的橙色错误。

/ *转型:“< S4 >: 75”* / / *转型:“< S4 >: 76”* /(我)+ +;/* Outport: '/FaultTable' */ polyspace_controller_demo_Y.FaultTable(*我]= 10;

您可以看到，错误是由于Stateflow图表中的转换而发生的synch_and_asynch_monitoring.您可以将错误跟踪到Stateflow图表的输入变量索引。

你可以避免越界数组索引在几个方面。一种方法是约束输入变量指数使用一个饱和在状态流图表前阻塞。

错误2:溢出

在结果列表窗格，选择橙色溢出错误如下所示。错误出现在文件中polyspace_controller_demo.c.

在源窗格，检查错误。要将错误追溯到模型，请单击链接S1 /增益在评论上面的橙色错误。

/ *获取:“< S1 > /增益”合并:* Inport: '/Battery Info' * Inport: '/Rotation' * Sum:“< S1 > / Sum1”* /增益=(int16_T) (((int16_T) ((in_rotation + in_battery_info) > > 1) * 24576) > > 10);

可以看到错误发生在故障管理子系统内部获得块后总和块。

你可以避免溢出在几个方面。一种方法是约束信号的值in_battery_info那是供给总和块。要限制信号:

双击Inport块电池信息它提供了输入信号in_battery_info到模型中。
在信号的属性选项卡中,改变最大信号的值。

这个模型中的错误是由于下列原因之一造成的:

错误的缩放，未知的校准和未经测试的数据范围从一个子系统进入一个算术块。
基于状态流事件的建模和手写查找表函数中的数组操作。
导致生成的代码中出现意外数据流的饱和。
错误的Stateflow编程。

一旦您确定了错误的根本原因，您就可以适当地修改模型来修复问题。

检查是否违反编码规则

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

在Polyspace选项卡上,选择设置.
在“配置参数”对话框中选择适当的选项设置从列表。例如,选择项目配置和MISRA C 2012 AGC检查.
建议您运行Bug Finder来检查MISRA C:2012规则。在Polyspace选项卡上,选择错误发现者.
点击应用或好吧并重新运行分析。

注释块以证明结果

您可以通过向块中添加注释来调整结果。在代码分析期间，Polyspace code Prover将读取您的注释并使用您的理由填充结果。一旦你证明一个结果是正确的，你就不需要再去检查它。

在结果列表窗格中，从左上角的下拉列表中选择文件.
在文件中polyspace_controller_demo.c，在函数中polyspace_controller_demo_step ()，选择违反MISRA C:2012规则10.4。的源窗格显示加法操作违反规则。
在源窗格，单击链接S1 / Sum1在加法运算上面的注释中。
```
/ *获取:“< S1 > /增益”合并:* Inport: '/Battery Info' * Inport: '/Rotation' * Sum:“< S1 > / Sum1”* /收益= (int16_T) (((int16_T) ((in_rotation + in_battery_info) > > 1) * 24576) > > 10);
```
您可以看到在Sum块中发生了违反规则的情况。

要注释此块并证明违反规则:
1. 选择块。在Polyspace选项卡上,选择添加注释.
2. 选择misra - c - 2012为注释类型并输入关于违反规则的信息。设置状态来任何行动计划和严重程度来设置.
3. 点击应用或好吧.这句话Polyspace注释出现在块的下面，表示该块包含一个代码注释。
4. 重新生成代码并重新运行分析。的严重程度和状态列在结果列表窗格中预先填充了您的注释。