高循环界限的数值分析
高循环界限的数值分析
提问于 2016-03-17 22:02:36
我正在分析一个具有以下结构的控制程序：
unsigned int cnt=0;
unsigned int inc=3;
...
void main(){
int i;
int lim;
for(i=0;i<100000;i++)
{
f1();
....
lim = f2();
if(cnt < lim)
cnt += inc;
....
}
}我的目标是分析足够的循环迭代，以证明cnt变量不能溢出。单独增加slevel不会有什么帮助，因为状态空间会变得太高。我看到slevel可以针对单个函数进行调整。例如，对于单个if/else构造，这也是可能的吗？对于这样的循环结构，增加整个函数的slevel可能已经太多了。有没有一种方法可以证明没有溢出，而不需要编写复杂的循环不变量和断言？
BR，Harald
回答 1
Stack Overflow用户
发布于 2016-03-18 04:28:00
我自作主张地指定f2返回一些正的值。否则，测试if(cnt < lim)将执行负的->无符号转换，该值目前不能准确处理。事实上，如果f2总是返回-1，那么你的属性就不成立！
在这个假设下，cnt不会溢出。
unsigned int cnt=0;
unsigned int inc=3;
//@ assigns \result \from \nothing; ensures 0 <= \result;
int f2();
void main(){
int i;
int lim;
for(i=0;i<100000;i++)
{
f1();
lim = f2();
if(cnt < lim)
cnt += inc;
}
}这是分析的结果。cnt没有溢出，因为它的最大值为4294967295。
[value] Values at end of function main:
cnt ∈ [0..2147483649],0%3
i ∈ {100000}
lim ∈ [0..2147483647]如果f2可以返回负值<= -4，我不确定是否可以在不使用WP插件的情况下验证结果。
关于你问题的其余部分，有多种选择可以更好地使用分析所需的slevel数量，但在这里可能没有任何帮助。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/36062837
复制相关文章
相似问题
腾讯云开发者
