2

我正在分析具有以下结构的控制程序：

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，哈拉尔

4

1 回答 1

1

我冒昧地指定f2返回一些积极的东西。否则，测试将if(cnt < lim)执行负 -> 无符号转换，目前 Value 无法精确处理。事实上，如果总是退货，您的财产将不成立！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 量，但在这里可能没有任何帮助。

于 2016-03-17T20:28:00.200 回答