主要内容

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

本教程演示了如何运行一个Polyspace®分析C / c++代码生成模型金宝app®模型。你也可以分析C / c++代码生成的一个子系统。完整的工作流程,请参阅采用嵌入式编码器生成Polyspace分析代码运行。

先决条件

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

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

openExample (“polyspace_code_prover / Op金宝appenSimulinkModelForPolyspaceAnalysisExample”)

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

这个示例使用:

打开脚本 
polyspace_controller_demo打开模型。

检查运行时生成的代码中的错误

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

  2. 在Polyspace选项卡上,选择代码验证在模式部分。

  3. 定位分析部分并选择代码生成模型从下拉列表中。

  4. 点击运行分析。Polyspace检查如果模型改变了自从上次代码生成。如果生成的代码是最新的,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);
更多信息关于跑步Polyspace分析MATLAB命令窗口,看到的pslinkoptions和pslinkrun。

回顾分析结果

在分析完成后,分析结果出现在Polyspace用户界面。结果由颜色编码的检查:

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

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

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

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

详细审查每个结果。在您的代码验证结果:

  1. 在结果列表窗格中,找到红色越限的数组索引检查。点击红色的检查(红点)。

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

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

跟踪和解决问题的模型

Polyspace问题报告生成的代码可能会引起的问题模型。跟踪一个问题回到你的模型来调查问题的根源。问题可能发生在代码中由于设计问题如:

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

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

  • 错误的编程等自定义代码块C函数和Stateflow块。

解决设计问题的示例模型,确定运行时错误的根源Polyspace报道:

非法取消引用指针

  1. 在结果列表窗格中,选择非法取消引用指针检查。

  2. 在源窗格中,单击链接< Root > /命令策略在上面的评论中错误。

    / * CFunction:“< Root > /命令策略”包含:* DataTypeConversion:“< S3 > / Cast4‘*尺寸:< Root > /电池信息‘* / / /…p = array [0];(我= 0;我< 100;我+ +){* p = 0;p =[1]代替;}rtb_x = (int16_T) ((uint16_T) rtb_y1 - in_battery_info);如果(rtb_x < 3) {rtb_x = (int16_T) (*p + 5);/ /……

强调了模金宝app型编辑器C函数这个错误出现的块。在这个街区,指针p增加100倍,指向* p外面的束缚数组。的非关联化操作rtb_x = (int16_T) (* p + 5);然后造成一个红色非法取消引用指针检查。

这个错误的一个解决方案是点* p后一个有效的内存位置为循环的C函数布洛克:

/ /循环后,点到一个有效的内存位置p = &(阵列[50]);/ /……tmp = * p + 5;

越限的数组索引

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

  2. 在源窗格中,单击链接< Root > /命令策略在上面的评论中错误。

    / * CFunction:“< Root > /命令策略”包含:* DataTypeConversion:“< S3 > / Cast4‘*尺寸:< Root > /电池信息‘* / / /…(我= 0;我< 100;我+ +){* p = 0;p =[1]代替;}/ /……如果((rtb_x > 92) & & (rtb_x < 110)){如果(another_array((rtb_x - i) + 9] ! = 0) {rtb_x = 92;其他}{rtb_x = 91;}}

强调了模金宝app型编辑器C函数这个错误出现的块。在这一块的价值我被设置为One hundred.在第一次为循环。该声明如果((rtb_x > 92) & & (rtb_x < 110))限制的可能值rtb_x来93 . . 109。在声明中another_array [(rtb_x - i) + 9] ! = 0可能的指标another_array范围从93 + 9 - 100 = 2来109 + 9 - 100 = 18。因为数组another_array只有两个元素,数组访问的another_array ((rtb_x - i) + 9)结果在一个红色的越限的数组索引运行时检查。

一个解决方案,这个错误是修改的通行条件rtb_x这样表达((rtb_x - i) + 9)计算结果为0或1。

如果((rtb_x > 91) & & (rtb_x < 93)){如果(another_array((rtb_x - i) + 9] ! = 0) {rtb_x = 92;其他}{rtb_x = 91;}}

橙色的检查

橙色代表运行时错误检查,可能发生在特定的代码执行路径。检查橙色检查和分类这些潜在问题的来源。例如:

  • 除零——这个橙色的两次检查报告。在声明中其中一个检查报告rtb_y1 = (int16_T) ((int16_T) (10 * 10)/(int16_T) (10 - rtb_x))。跟踪的原因可能错误,点击发表评论< S6 > /鸿沟。强调了模金宝app型编辑器分块。的执行路径÷输入= 0,该部门操作结果除零错误。

    要解决这个错误,检查÷输入不为零。例如,使用如果(金宝app模型)块,把分块在一个如果行动子系统(金宝app模型)。

    另一个除零检查可以使用类似的技术来解决检查分母为零。

  • 绑定数组索引声明:这个橙色的检查报告polyspace_controller_demo_Y.FaultTable(*我]= 10;。跟踪这个潜在错误的根源,点击链接S4:76在上面的评论中橙色的错误。强调了模金宝app型编辑器Stateflow图表synch_and_asynch_monitoring。跟踪错误的输入变量指数Stateflow图表。

    一个解决方案,以避免这张支票是限制输入变量指数。使用一个饱和块之前Stateflow图表限制的价值指数从零到One hundred.。

  • 溢出:Polyspace报告几个橘子溢出检查。解决这些检查通过约束输入。例如,考虑到橙色溢出检查在声明中rtb_k =(int16_T) (((int16_T) ((in_rotation + in_battery_info) > > 1) * 24576) > > 10)。跟踪检查模型,点击链接S1 /增益在上面的评论中橙色的检查。强调了模金宝app型编辑器获得块的故障管理子系统。

    一个解决方案以避免橙色溢出checkk是限制信号的值in_battery_info这是美联储总和块。例如:

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

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

    使用这种技术来解决类似的橙色溢出检查。

检查编码规则违规

检查编码规则的违反,开始Polyspace错误发现者™分析。

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

  2. 在模式部分中,选择错误发现者。

  3. 重新运行分析。

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

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

注释块来证明的结果

来证明Polyspace结果,添加注释块。在代码分析,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. 重新生成代码并重新运行分析。的严重程度和状态列在结果列表面板现在来填充你的注解。

相关的话题