1

是否有任何“几乎可用”的 C（或类似 C）程序的静态分析工具可以自动推断循环终止，至少对于非常简单的程序？

我环顾四周，发现了几篇研究文章、一些原型，甚至还有一些工具（例如Frama-C），它们试图从带注释的源代码中推断出一些终止属性，但我希望至少能找到一个简单的工具你可以给它一个 C 程序，它会输出：loop #N terminates// does not terminate。unknown

（我知道这在一般情况下是无法确定的，但对于某些类别的循环，半算法是可能的）。

我还对适用于 C 以外的命令式语言（例如 Java）的工具感兴趣。

编辑：只是对我的问题的更新，我发现LoopF​​rog建立在goto-cc之上，这似乎是我正在寻找的方向，但是我仍然没有时间真正理解它的输出意味着什么恰恰。如果它是我问题的答案，我会在这里发布更新。

4

1 回答 1

1

我不知道您是否阅读过这两篇博文（1、2 ），但您正在寻找的“简单”工具之一可能是一个脚本，它同时启动 Frama-C 的价值分析作为普通声音抽象解释器（能够推断程序的结尾不可达）和它的选项-obviously-terminates（在这种情况下，它可以推断程序的所有执行都终止）。在这两种情况下，您可能都想使用超时。对于带有选项的分析-obviously-terminates，超时是强制性的，因为如果分析的程序本身没有终止，分析将无法终止。

根据我写的这些博客文章，您应该能够诊断出以下示例，并非所有示例都是微不足道的：

char x, y;

main()
{
  x = input();
  y = input();
  while (x>0 && y>0)
    {
      if (input() == 1)
    {
      x = x - 1;
      y = input();
    }
      else
    y = y - 1;
    }
}

终止

char x, y;

main()
{
  x = input();
  y = input();

  while (x>0 && y>0)
    {
      // Frama_C_dump_each();
      if (input())
        {
          x = x - 1;
          y = x;
        }
      else
        {
          x = y - 2;
          y = x + 1;
        }
    }
}

终止

char x;

main(){
  x = input();
  while (x > 0)
    {
      Frama_C_dump_each();
      if (x > 11)
        x = x - 12;
      else
        x = x + 1;
    }
}

终止

unsigned char u;

int main(){
  while (u * u != 17)
    {
      u = u + 1;
    }
  return u;
}

不终止。

但是，-obviously-terminates这些示例中涉及的选项最初并不是为这种用途而设计的（它更多的是对某种程序的分析进行优化）。我没有意识到在极少数情况下，当设置此选项时，分析可能会终止，而被分析的程序本身不会终止。如果您愿意从源代码重新编译，则可以通过在 file中将 variable 设置obviously_terminates为true（而不是）来解决此问题。如果您有理由认为此脚本不是您正在寻找的解决方案，请不要打扰：正如我所说，这个问题似乎很少见。我只是在试图确定程序是否在更具竞争性的环境中终止时才注意到它。falsestate_set.ml

于 2012-11-29T20:40:41.807 回答