2

いくつかの ACSL アサーションを含むファイルがあります ( file.c):

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

void foo()    {
  int a=0;
  //@ assert(a==0);
}

void print(const char* text)   {
    int a=0;
    //@ assert(a==0);
    printf("%s\n",text);
}

int main (int argc, const char* argv[])    {
    const char* a1 = argv[2];

    print(a1);
    foo();

    if (!a1)
      //@ assert(!a1);
        return 0;
    else
        return 1;
}

次のコマンドですべてのアサーションをスライスしたい:

frama-c -slice-assert @all file.c -then-on 'Slicing export' -print -ocode slice.c

ただし、スライスは期待どおりに見えません (実際には、ファイルに含まれる関数はまったく含まれていません)。

/* Generated by Frama-C */
typedef unsigned int size_t;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */

/*@
axiomatic dynamic_allocation {
  predicate is_allocable{L}(size_t n) 
    reads __fc_heap_status;

  }
 */
void main(void)
{
  char const *a1;
  return;
}

代わりに、次のような出力が得られます。

file.c:16:[kernel] warning: out of bounds read. assert \valid_read(argv+2);
[value] Recording results for main
[value] done for function main
file.c:16:[value] Assertion 'Value,mem_access' got final status invalid.
[slicing] making slicing project 'Slicing'...
[slicing] interpreting slicing requests from the command line...
[pdg] computing for function foo
[pdg] warning: unreachable entry point (sid:1, function foo)
[pdg] Bottom for function foo
[slicing] bottom PDG for function 'foo': ignore selection
[pdg] computing for function main
file.c:21:[pdg] warning: no final state. Probably unreachable...
[pdg] done for function main
[pdg] computing for function print
[pdg] warning: unreachable entry point (sid:5, function print)
[pdg] Bottom for function print
[slicing] bottom PDG for function 'print': ignore selection

ここで何がうまくいかないのか、特に、何をしunreachable entry pointますか? 観察: に変更argv[2]するargv[1]と、これらの問題は発生しません (ただし、最初の行で警告が表示されます)。

4

1 に答える 1

3

スライスでは、Value 分析結果を使用する PDG (Program Dependent Graph) を計算する必要があります。警告unreachable entry pointは、指定したコンテキストでは関数fooに到達できないことを意味します (つまり、到達できないステートメントから呼び出されます)。

例を挙げずにこれ以上説明するのは難しい...

編集：

提供した出力で、次の行に注目してください。

file.c:16:[kernel] warning: out of bounds read. assert \valid_read(argv+2);

と

file.c:16:[value] Assertion 'Value,mem_access' got final status invalid.

値分析が無効なプロパティに遭遇すると、それ以上進むことができません。ここでは最初のステートメントからアラームが発生するため、他のすべては到達不能になります。無効なプロパティは\valid_read(argv+2);、入力コンテキストのデフォルトが の幅 2 であるためargvです。これは、オプション を使用するか、引数を取らず、明示的に定義し、実数を呼び出す-context-width 3解析用の別のエントリ ポイントを使用する (および で指定する)ことで修正できます。-main my_mainargcargvmain

アドバイスは、値分析の結果が問題ないかどうかを確認した後でのみ、スライスを使用することです。オプションを使用して単独で実行し、-val必要に応じて他のオプションを調整できます。

于 2016-07-27T08:41:13.977 に答える