2

printf 呼び出しで次のプログラムをスライスしようとしています。

#include <stdlib.h>
#include <stdio.h>

int main(int argc, char **argv) {

  if (argc < 3) return 1;

  int x = atoi(argv[1]);
  int y = atoi(argv[2]);

  printf("%d %d\n", x, y);

  return 0;
}

ただし、Value Analysis プラグインは次のメッセージを表示します。

foo.c:9:[value] 関数呼び出し式の引数 (char const )の評価で非終了(argv + 2),

スライスされたプログラムは空です！これは Frama-C のバグ/機能ですか? それとも私は何か間違ったことをしていますか？

完全なトレースは次のとおりです。

$ frama-c -slice-calls printf foo.c -then-on 'Slicing export' -print
[slicing] slicing requests in progress...
[kernel] preprocessing with "gcc -C -E -I.  foo.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
foo.c:8:[kernel] warning: out of bounds read. assert \valid(argv+1);
[value] computing for function atoi <- main.
        Called from foo.c:8.
[kernel] warning: No code for function atoi, default assigns generated
[value] Done for function atoi
foo.c:9:[kernel] warning: out of bounds read. assert \valid(argv+2);
foo.c:9:[value] Non-termination in evaluation of function call expression argument
        (char const *)*(argv + 2)
[value] Recording results for main
[value] done for function main
[slicing] making slicing project 'Slicing'...
[slicing] interpreting slicing requests from the command line...
[slicing] applying all slicing requests...
[slicing] applying 0 actions...
[slicing] exporting project to 'Slicing export'...
[slicing] applying all slicing requests...
[slicing] applying 0 actions...
[sparecode] remove unused global declarations from project 'Slicing export tmp'
[sparecode] removed unused global declarations in new project 'Slicing export'
/* Generated by Frama-C */
4

1 に答える 1

2

価値分析マニュアルの 5.2.3 不完全なアプリケーションの分析を参照してください。

ポインター型の変数の場合、ポインターが単一の要素を指していると見なすべきか、それとも配列の先頭を指していると見なすべきか、あるいは配列の途中を指していると見なすべきかをアナライザーが推測する方法はありません。 、これは、このポインターの負のオフセットを取ることが合法であることを意味します。既定では、ポインター型は 2 つの要素の配列の先頭を指すと見なされます。この数はオプションで変更できます-context-width。例: エントリ ポイントのプロトタイプが の場合void main(int *t)、アナライザーはt配列 を指していると想定しint S_t[2]ます。

argv同じことが、プログラムのmain()関数の引数にも当てはまります。マニュアルの他の場所で説明されているように、実際に引数に対応すると予想されるポインターの適切な配列をmain()作成します (例: main_2.c 23 ページ)。0 ～ 1000 の範囲の整形式の整数についてプログラムを検証またはスライスするだけの場合は、 を割り当てた/*@ assert 0 <= x <= 1000 ; */後にプログラムに挿入できます。x

[カーネル] 警告: 関数 atoi のコードがありません。デフォルトの割り当てが生成されます

同じマニュアルの2.3.3 Missing functionsもお読みください。というか、まずマニュアルを読んでから、価値分析とスライスのプラグインを使ってみてください。これは、今日のソフトウェアの学習曲線が急勾配ですが、実際には、それが意図された使用方法です。

とにかく、アナライザーが遭遇するすべての機能に対して、実装または最小限の仕様を提供する必要があります。Frama-C の最新のリリースには、share/libc に多くの標準機能の優れた仕様が含まれており、コンピュータの /usr/local/lib/Frama-C/libc にインストールされている可能性があります。

于 2014-05-21T18:11:50.750 に答える