运行Polyspace生成的代码分析金宝app模型
您可以运行Polyspace®从Simulink生成的代码金宝app®模型或子系统。
Polyspace错误发现者™检查代码中的bug或代码规则违反情况(例如，MISRA C®: 2012条规则)。
Polyspace代码验证™全面检查代码是否存在运行时错误。
如果你使用嵌入式编码器®对于代码生成，本教程展示了如何在一个简单的Simulink模型生成的代码上运行Polyspace。金宝app有关完整的工作流，请参见对用嵌入式编码器生成的代码运行多空间分析。
先决条件
在从Simulink运行Polyspace之前，必须将Pol金宝appyspace和MATLAB连接起来®安装。看到将Polyspace与MATLAB和Simulink集成金宝app。
要打开本例中使用的模型，请在MATLAB命令窗口中运行:
openExample (“polyspace_code_prover / OpenModelForCodeGenerationAndPolyspaceAnalysisExample”)
代码生成和多空间分析的开放模型
打开模型polyspace_controller_demo用于配置代码生成和Polyspace分析。
生成和分析代码
要开始对模型生成的代码进行Polyspace分析:
在应用程序选项卡上,选择Polyspace代码验证器。
在Polyspace选项卡,找到分析字段和选择代码生成为Top模型从下拉菜单。
点击画布上的任何地方。的分析代码字段显示模型名称。选择运行分析。
当您单击时，Polyspace检查生成的代码运行分析。如果没有生成的代码，Polyspace首先使用Embedded Coder生成代码，然后开始分析。
等价的MATLAB代码：
load_system (“polyspace_controller_demo”）;slbuild (“polyspace_controller_demo”）;mlopts = pslinkoptions (“polyspace_controller_demo”）;mlopts。ResultDir =“\结果”mlopts。VerificationMode =“CodeProver”；pslinkrun (“polyspace_controller_demo”, mlopts);
CodeProver与BugFinder。有关代码的更多信息，请参见pslinkoptions和pslinkrun。
回顾分析结果
分析后，结果显示在Polyspace用户界面中。
如果您运行Bug Finder，则结果由在生成的代码中检测到的Bug组成。如果你运行代码验证程序，结果由如下颜色编码的检查组成:
绿色(证明代码):对于提供的数据约束，检查不会失败。例如，除法操作不会导致除零错误。
红色(验证错误):对于所提供的数据约束集，检查总是失败。例如，除法运算总是导致除零错误。
橙色(可能的错误):该检查指示未经验证的代码，对于所提供的数据约束的某些值可能会失败。例如，除法运算有时会导致除零错误。
灰色(不可到达的代码):该检查表示无法获取所提供的数据约束的代码操作。
详细审查每个分析结果。例如，在你的代码验证结果:
在结果列表窗格中，选择红色数组索引越界检查。
在源窗格中，将光标放在红色复选框上以查看其他信息。例如，红色的工具提示
［操作符声明数组大小和数组索引的可能值。的结果细节窗格也提供此信息。
错误发生在手写的C文件中Command_strategy_file.c。C文件位于s函数块中Command_Strategy在降低了精度子系统(在模型引用中)相对阈值)．
跟踪错误到模型并修复它们
对于从模型生成的代码，您可以跟踪一个错误到您的模型。这些部分展示了如何跟踪特定的Code Prover结果到模型。
错误1:数组索引越界
在结果列表窗格，选择橙色数组索引越界文件中发生的错误
polyspace_controller_demo.c。在源窗格，单击链接S4:76在橙色错误的注释上面。
/ *转型:“< S4 >: 75”* / / *转型:“< S4 >: 76”* /(我)+ +;/* Outport: '
/FaultTable' */FaultTable［*我]= 10;
您可以看到，错误是由于状态流程图中的转换而发生的synch_and_asynch_monitoring。您可以跟踪错误到状态流图的输入变量索引。
你可以避免数组索引越界在几个方面。一种方法是约束输入变量指数使用一个饱和块前面的状态流程图。
错误2:溢出
在结果列表窗格，选择橙色溢出错误如下所示。错误出现在文件中
polyspace_controller_demo.c。在源窗格，检查错误。要将错误跟踪回模型，请单击链接S1 /增益在橙色错误的注释上面。
可以看到错误发生在/ *获取:“< S1 > /增益”合并:* import: '
/Battery Info' * import: ' /Rotation' * Sum:“< S1 > / Sum1”* /增益=（int16_T) (((int16_T) ((in_rotation + in_battery_info) > > 1) * 24576) > > 10); 故障管理子系统内部获得块后总和块。
你可以避免溢出在几个方面。一种方法是限制信号的值in_battery_info那是喂给总和块。限制信号:
双击import块
电池信息它提供输入信号in_battery_info到模型中。在信号的属性选项卡中,改变最大信号的值。
该模型中的错误是由于以下原因之一引起的:
错误的缩放，未知的校准和未经测试的数据范围从一个子系统进入一个算术块。
基于statflow事件的建模和手写查找表函数中的数组操作。
饱和导致生成的代码中出现意想不到的数据流。
错误的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 > /增益”合并:* import: '
/Battery Info' * import: ' /Rotation' * Sum:“< S1 > / Sum1”* /收益= (int16_T) (((int16_T) ((in_rotation + in_battery_info) > > 1) * 24576) > > 10); 您可以看到在Sum块中发生了规则违反。
注释此块并证明违反规则:
选择块。在Polyspace选项卡上,选择添加注释。
选择
misra - c - 2012为注释类型并输入违规信息。设置状态来任何行动计划和严重程度来设置。点击应用或好吧。这句话Polyspace注释出现在代码块下面，表示该代码块包含代码注释。
重新生成代码并重新运行分析。的严重程度和状态列在结果列表窗格中预先填充了您的注释。
相关的话题
你也可以从以下列表中选择一个网站:
