3

C ファイルが与えられた場合、いくつかの基準について後方スライスを計算し、そのスライスを元のコードと比較したいと考えています。最初からスライシング プログラムを実装したくないので、このタスクに役立つと思われる Frama-C に慣れようとしました。

ただし、私の問題は、Frama-C のスライス プラグインが前処理された入力コードを変更するため、元のどの行がスライスにも表示されるかを識別するのが難しくなることです。

例：

入力ファイルtest1.c:

double func1(double param) {
    return 2+param;
}

int main() {
    int a=3;
    double c=4.0;
    double d=10.0;
    if(a<c)
        c=(double)a/4.0;
    double res = func1(c);
    return 0;
}

前処理されたファイル (によって生成frama-c test1.c -print -ocode test1_norm.c):

/* Generated by Frama-C */
double func1(double param)
{
  double __retres;
  __retres = (double)2 + param;
  return __retres;
}

int main(void)
{
  int __retres;
  int a;
  double c;
  double d;
  double res;
  a = 3;
  c = 4.0;
  d = 10.0;
  if ((double)a < c) c = (double)a / 4.0;
  res = func1(c);
  __retres = 0;
  return __retres;
}

スライス ( によって生成frama-c -slice-calls func1 test1.c -then-on 'Slicing export' -print):

/* Generated by Frama-C */
double func1_slice_1(double param)
{
  double __retres;
  __retres = (double)2 + param;
  return __retres;
}

void main(void)
{
  int a;
  double c;
  double res;
  a = 3;
  c = 4.0;
  c = (double)a / 4.0;
  res = func1_slice_1(c);
  return;
}

の署名がmain異なり、 の名前がfunc1に変更されたことに注意してくださいfunc1_slice_1。

スライスと（前処理された）オリジナルを（計算可能な差分に関して）より簡単に比較できるようにするために、その動作を抑制する方法はありますか？

4

1 に答える 1

2

最初に、あなたが答える必要はないが、同じキーワードを検索している人は答えることができるという単純な質問を明確にするために、スライスされたプログラムを元のプログラムの行の選択として印刷することはできません (2 つの違いのほとんどは対応しています)。情報がそこにあれば、可能な限り最も類似したプログラムを印刷するために使用されます)。あなたができることは、元のプログラムの Frama-C の表現を印刷することですframa-c test2.c -print -ocode test2_norm.c。

func1に名前が変更されるという問題を解決するにはfunc1_slice_1、オプションで試してみてください-slicing-level 0。

$ frama-c -slicing-level 0 -slice-calls func1 test1.c -then-on 'Slicing export' -print
...
/* Generated by Frama-C */
double func1(double param)
{
  double __retres;
  __retres = (double)2 + param;
  return __retres;
}

void main(void)
{
  int a;
  double c;
  double res;
  a = 3;
  c = 4.0;
  c = (double)a / 4.0;
  res = func1(c);
  return;
}

これにより、スライサーが内部をスライスするのをまったく防ぐことができると思いますfunc1。ヘルプには次のように書かれています。

-slicing-level <n> に伝播するために使用されるスライスのデフォルト レベルを設定します。
                    通話
                    0 : 呼び出された関数をスライスしない
                    1 : 呼び出された関数をスライスせずに伝播します。
                    とにかくマーク
                    2 : 既存のスライスを使用してみてください。多くても 1 つ作成してください
                    3 : 最も正確なスライス
于 2016-03-04T10:56:44.063 に答える