MATLAB的答案

Polyspace代码,配置DRS,即使一个用户定义的函数的参数初始化和“Init范围”,它不是在验证情感

12个视图(30天)
Praveen Nerji
Praveen Nerji 2015年9月28日
回答: 马特·罗兹 2017年5月15日
如果真正的
Func1 (__arg1、最长长度)
{
…。
…。
局部变量= __arg1 +最长;
如果(长度> = 200)
{
/ * * /做某事/不遥不可及的代码
}
}
main ()
{
…
Func1 (20100);
}
结束
在DRS配置、初始化的长度是200。项目配置为在整个应用程序级验证。
但是长度不是在200年期间核查。在检查细节/提示指出,考虑到只有100。
要求:为了测试我的保护代码(错误标志检查情况),请提供一个解决方案

在回答这个问题。

答案(1)

马特·罗兹
马特·罗兹 2017年5月15日
嗨Jyothi -
有 两种不同的冲突的配置设置 这里发生了:
  1. DRS的配置,也被称为约束规范,使用主发电机告诉主发电机如何限制调用函数。
  2. 选择“验证整个应用程序”意味着Polyspace正在等你提供主要()分析,你正在做的事情。
换句话说,你必须告诉Polyspace“验证模块或者库”而不是“验证整个应用程序。”I also see that you are providing a main in your example code. When you do this, Polyspace sees the main you provide and overrides your setting to be "Verify Whole Application" because it cannot correctly resolve which main to use on its own. You will have to either exclude the main you are providing, or use a MACRO to rename main so that Polyspace can use its own main generator.
一个想法。 如果您使用的是你的主,你所看到的论点与100年而不是200年被初始化,这是因为你的主要是100年导致初始化。如果你实际上是使用100年而不是200年,你有什么理由试图让Polyspace来初始化这个值200 ?