主要内容

多空间基于web的代码生成分析金宝app模型

您可以运行Polyspace®关于Simulink生成的代码金宝app®模型或子系统。

  • 多空间Bug查找器™检查代码是否存在错误或违反编码规则(例如,MISRA C®:2012年规则)。

  • 多空间码验证器™彻底检查代码的运行时错误。

如果你使用嵌入式编码器®对于代码生成,本教程介绍如何在从简单Simulink模型生成的代码上运行Polyspace。有关完整的工作流,请参阅金宝app对使用嵌入式编码器生成的代码运行多空间分析.

先决条件

在从Simulink运行Polyspace之前,必须将Pol金宝appyspace与MATLAB链接起来®安装。请参阅利用MATLAB和Simulink集成Polyspace金宝app.

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

开瓶器示例(“polyspace\代码\验证程序/OpenModelForCodeGeneration和polyspace分析示例”)

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

打开模型多空间控制器演示用于配置代码生成和多空间分析。

生成和分析代码

要开始对模型生成的代码进行多空间分析,请执行以下操作:

  1. 应用程序选项卡,选择多空间码校验器.

  2. 多空间选项卡,找到分析字段并选择作为顶级模型生成的代码从下拉菜单中。

  3. 单击画布上的任意位置从中分析代码字段显示模型名称。选择运行分析.

单击时,Polyspace会检查生成的代码运行分析。如果不存在生成的代码,则Polyspace首先使用嵌入式编码器生成代码,然后开始分析。

等效MATLAB代码:

加载系统(“polyspace\u控制器\u演示”); slbuild(“polyspace\u控制器\u演示”);mlopts=pslinkoptions(“polyspace\u控制器\u演示”);mlopts.ResultDir=“\result”mlopts.VerificationMode=“代码验证程序”; pslinkrun(“polyspace\u控制器\u演示”,mlopts);
要使用Bug Finder进行分析,请替换编码器具有窃贼。有关代码的详细信息,请参阅pslinkoptionspslinkrun.

审查分析结果

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

如果运行Bug Finder,结果将由在生成的代码中检测到的Bug组成。如果运行代码验证程序,结果由以下颜色编码的检查组成:

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

  • 红色(已验证错误):对于提供的一组数据约束,检查总是失败。例如,除法操作总是导致除零错误

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

  • 灰色(无法访问的代码):该检查指示无法针对提供的数据约束执行的代码操作。

详细查看每个分析结果。例如,在代码验证程序结果中:

  1. 成绩表窗格中,选择红色越界数组索引检查

  2. 来源窗格中,将光标放在红色复选框上以查看其他信息。例如,红色复选框上的工具提示[运算符说明数组大小和数组索引的可能值结果详情窗格还提供了此信息。

该错误发生在手写C文件中命令\u策略\u文件.c. C文件位于S函数块内指挥部战略降低精度子系统(在模型参考中)相对阈值).

将错误追溯到模型并修复它们

对于从模型生成的代码,您可以将错误追溯到您的模型。这些部分说明如何将特定的代码验证程序结果追溯到模型。

错误1:超出范围的数组索引

  1. 成绩表窗格中,选择橙色越界数组索引文件中发生的错误polyspace\u控制器\u演示.c.

  2. 来源窗格中,单击链接S4:76在上面的注释中出现橙色错误。

    /*过渡::75”*//*过渡::76”*/(*i)++/*输出端口:'/FaultTable'*/polyspace\u controller\u demo\u Y.FaultTable[*i] =10;

您可以看到,该错误是由于状态流程图中的转换而发生的同步和异步监视。您可以将错误跟踪到状态流程图的输入变量索引。

你可以避免越界数组索引有几种方法。一种方法是约束输入变量指数使用饱和状态流程图前的块。

错误2:溢出

  1. 成绩表窗格中,选择橙色溢流错误如下所示。错误出现在文件中polyspace\u控制器\u演示.c.

  2. 来源窗格中,查看错误。若要将错误追溯到模型,请单击链接S1/增益在上面的注释中出现橙色错误。

    /*收益:/增益”合并:*输入端口:“/Battery Info”*输入端口:“/Rotation”*总和:/Sum1”*/获得=(int16_T)(((int16_T)((in_旋转+in_电池信息)>>1)*24576)>>10);
    您可以看到错误发生在故障管理内部子系统获得紧跟着一个总和

你可以避免溢流在几个方面。一种方法是限制信号的值电池信息这是喂给孩子们的总和块要限制信号,请执行以下操作:

  1. 双击输入块电池信息它提供输入信号电池信息与模型相一致。

  2. 信号属性选项卡,更改最大限度信号的值。

此模型中的错误是由于以下原因之一造成的:

  • 从子系统输出的错误缩放、未知校准和未测试数据范围进入算术块。

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

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

  • 错误的状态流编程。

一旦确定了错误的根本原因,就可以适当地修改模型以解决问题。

检查是否存在编码规则冲突

要在开始代码分析之前检查编码规则冲突,请执行以下操作:

  1. 多空间选项卡,选择设置.

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

    建议您运行Bug Finder来检查MISRA C:2012规则多空间选项卡,选择Bug查找器.

  3. 点击申请好啊然后重新运行分析。

注释块以对齐结果

您可以通过向块中添加注释来对结果进行对正。在代码分析过程中,Polyspace code Prover会读取您的注释并使用对正填充结果。对结果进行对正后,您无需再次查看。

  1. 成绩表窗格中,从左上角的下拉列表中选择文件.

  2. 在文件中polyspace\u控制器\u演示.c,在函数中polyspace_控制器_演示_步骤(),选择违反MISRA C:2012第10.4条规则的情况来源窗格显示添加操作违反规则。

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

    /*收益:/增益”合并:*输入端口:“/Battery Info”*输入端口:“/Rotation”*总和:/Sum1”*/增益=(int16_T)((int16_T)((in_旋转+in_电池信息)>>1)*24576)>>10);

    您可以看到规则冲突发生在Sum块中。

    要对此块进行注释并证明违反规则是正确的,请执行以下操作:

    1. 选择块。在多空间选项卡,选择添加注释.

    2. 选择MISRA-C-2012对于注释类型并输入有关违反规则的信息。设置地位没有计划采取行动严重程度取消.

    3. 点击申请好啊.文字多空间注释显示在块下方,指示块包含代码注释。

    4. 重新生成代码并重新运行分析严重程度地位上的列成绩表窗格中预先填充了注释。

相关话题