1

少なくとも非常に単純なプログラムの場合、ループの終了を自動的に推測できるC（またはCのような）プログラム用の「ほぼ使用可能な」静的分析ツールはありますか？

少し調べてみると、いくつかの研究記事、いくつかのプロトタイプ、さらには注釈付きのソースコードからいくつかの終了プロパティを推測しようとするいくつかのツール（ Frama-Cなど）が見つかりましたが、少なくとも1つの簡単なツールを見つけることを期待していましたCプログラムを指定すると、次のように出力されます：loop #N terminates// 。does not terminateunknown

（これは一般的なケースでは決定不可能ですが、ループのクラスによっては半アルゴリズムが可能です）。

また、JavaなどのC以外の命令型言語で機能するツールにも興味があります。

編集：私の質問の更新だけで、goto-ccの上に構築されたLoopF​​rogを見つけました。これは私が探していた方向にあるようですが、それでもその出力が何を意味するのかを実際に理解する時間がありませんでした正確に。それが私の質問への答えであるならば、私はここに更新を投稿します。

4

1 に答える 1

1

これらの2 つのブログ投稿 (1、2 )を読んだかどうかはわかりませんが、探している「単純な」ツールの 1 つは、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 で variableobviously_terminatesをtrue(の代わりにfalse) に設定することで修正されますstate_set.ml。このスクリプトが探している解決策ではないと考える理由がある場合でも、心配する必要はありません。前述したように、この問題はまれにしか発生しないようです。プログラムがより競争力のある設定で終了したかどうかを判断しようとしているときに、私はそれに気づきました.

于 2012-11-29T20:40:41.807 に答える