主要内容

运行Polyspace分析代码生成金宝app模型

您可以运行一个Polyspace®分析从模型生成的代码金宝app®模型或子系统。

  • Polyspace错误发现者™检查错误的代码或编码规则违规。

  • Polyspace代码验证™详尽检查运行时错误的代码。

本教程演示了如何运行一个Polyspace分析仿真软件模型生成的代码。金宝app完整的工作流程,请参阅采用嵌入式编码器生成Polyspace分析代码运行。

先决条件

从仿真软件运行Polyspace之前,你必须联系Polysp金宝appace和MATLAB®安装。看到用MATLAB和Simulink Polyspace集成金宝app。

开在这个示例中,使用的模型在MATLAB命令窗口,运行:

openExample (“polyspace_code_prover / Op金宝appenSimulinkModelForPolyspaceAnalysisExample”)

打开Pol金宝appyspace分析仿真软件模型

这个示例使用:

打开脚本 
polyspace_controller_demo打开模型。

生成和分析代码

  1. 在应用程序选项卡上,选择Polyspace代码验证器。

  2. 在Polyspace选项卡,找到分析字段和选择代码生成模型从下拉列表中。

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

    Polyspace开始代码验证分析。

当你点击运行分析生成的代码,代码验证检查。如果没有生成的代码,Polyspace首先生成的代码通过使用嵌入式编码器®,然后开始分析。

另外,在MATLAB命令窗口中,输入:

%负荷模型load_system (“polyspace_controller_demo”);%生成代码slbuild (“polyspace_controller_demo”);%创建Polyspace选择对象mlopts = pslinkoptions (“polyspace_controller_demo”);%结果指定文件夹mlopts。ResultDir =“\ cp_result”;%设置分析代码验证模式mlopts。VerificationMode =“CodeProver”;%运行分析pslinkrun (“polyspace_controller_demo”,mlopts);
看到pslinkoptions和pslinkrun。

回顾分析结果

分析完成后,打开Polyspace用户界面显示结果。结果由不同颜色的检查:

  • 绿色(证明代码)数据约束:检查不失败。例如,一个部门操作不会引起除零错误。

  • 红色(验证错误):检查总是失败的一组数据约束。例如,一个部门操作总是引起除零错误。

  • 橙色(可能的错误):检查表明未经证实的代码,可以失败对于某些值提供的数据约束。例如,一个部门操作有时会导致除零错误。

  • 灰色(不可到达的代码):检查表明代码操作,不能提供的数据约束。

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

  1. 在结果列表窗格中,选择红色越限的数组索引检查。

  2. 在源窗格中,将鼠标放在红色检查查看更多信息。例如,工具提示在红(符数组大小和可能的值数组的索引。的结果细节窗格中还提供了这些信息。

两个红色检查发生在手写的C代码C函数块Command_Strategy。

跟踪和解决问题的模型

错误代码生成自模型在模型中所引起的问题。跟踪一个错误回到你的模型来调查问题的根源。

错误1:界外数组索引

  1. 在结果列表窗格中,选择橙色越限的数组索引错误发生在该文件polyspace_controller_demo.c。

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

    / *转型:“< S4 >: 75”* / / *转型:“< S4 >: 76”* /(我)+ +;/ *输出港:“< Root > / FaultTable”* / polyspace_controller_demo_Y.FaultTable(*我]= 10;

模型编辑金宝app器中突显出这个错误的起源。在这种情况下,错误发生由于过渡Stateflow图表synch_and_asynch_monitoring。跟踪错误的输入变量指数Stateflow图表。

一个可能的解决方案,以避免橙色越限的数组索引违反约束输入变量指数。使用一个饱和块之前Stateflow图表来限制指数零到One hundred.。运行修改后的模型分析后,橙色检查解决。

错误2:溢出

  1. 在结果列表窗格中,选择橙色溢出错误代码所示。文件中出现的错误polyspace_controller_demo.c。

    / *获取:“< S1 > /增益”包含:*尺寸:< Root > /电池信息的*尺寸:“< Root > /旋转”*总和:“< S1 > / Sum1”* / rtb_k =(int16_T) (((int16_T) ((in_rotation + in_battery_info) > > 1) * 24576) > > 10);

  2. 在源面板,检查错误。跟踪误差模型,点击链接S1 /增益上面的评论中橙色的错误。模型编辑金宝app器中突显出这个错误的起源。在这种情况下,错误发生在故障管理子系统内部获得块后总和块。

一个可能的解决方案,以避免橙色溢出错误是限制信号的值in_battery_info这是美联储总和块。

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

  2. 在信号的属性选项卡中,改变最大信号到一个较低的价值,价值等500年。

运行修改后的模型分析后,橙色检查解决。

在这个模型中发生的错误由于其中一个设计问题:

  • 错误的比例、未知的校准和测试数据范围的一个子系统为一个算术。

  • 数组操纵Stateflow基于事件的建模和手写的查找表的功能。

  • 饱和度的导致意想不到的内部数据流生成的代码。

  • 错误的Stateflow编程。

一旦你确定错误的根源,你可以适当地修改模型来解决这个问题。

检查编码规则违规

开始一个Bug仪分析检查编码规则违规。

  1. 在Polyspace选项卡上,选择设置>项目设置并支持MISRA - C: 2012编码标准编码标准和代码度量节点。保存配置并关闭窗口。

  2. 在Polyspace选项卡上,选择错误发现者。

  3. 点击应用或好吧并重新运行分析。

另外,在MATLAB命令窗口中,输入:

%使检查MISRA - C: 2012 mlopts受侵犯。VerificationSettings =“PrjConfigAndMisraC2012”;%为Bug仪分析mlopts指定单独的文件夹。ResultDir = ' \ bf_result ';%设置分析Bug mlopts仪模式。VerificationMode =“BugFinder”;%运行分析pslinkrun (polyspace_controller_demo, mlopts);
分析完成后,打开Polyspace UI包含一系列MISRA - C: 2012违反规则的行为。

注释块来证明的结果

你可以证明你的结果通过添加注释块。在代码分析,Polyspace填充结果与你的理由。一旦你证明结果,你不需要审查一遍。

  1. 在结果列表窗格中,在左上角,从下拉列表中选择文件。

  2. 在文件中polyspace_controller_demo.c在函数中,polyspace_controller_demo_step (),选择违反MISRA - C: 2012规则10.4。的源加法操作窗格中显示,违反了规则。

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

    / *获取:“< S1 > /增益”包含:*尺寸:< Root > /电池信息的*尺寸:“< Root > /旋转”*总和:“< S1 > / Sum1”* / rtb_k = (int16_T) (((int16_T) ((in_rotation + in_battery_info) > > 1) * 24576) > > 10);

    违反规则的出现在一个块求和。

  4. 注释块和证明违反规则:

    1. 选择块。在Polyspace选项卡上,选择添加注释。

    2. 选择misra - c - 2012为注释类型并输入关于违反规则的信息。设置状态来任何行动计划和严重程度来设置。

    3. 点击应用或好吧。这句话Polyspace注释出现以下的块,这表明包含一个代码块注释。

  5. 重新生成代码并重新运行分析。的严重程度和状态列在结果列表窗格来填充你的注释。

相关的话题