「到達不能なエントリポイント」というメッセージは何を意味していますか？

Question

私はいくつかの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]に変更すると、私はこれらの問題は発生しません（ただし、最初の行には警告が表示されます）。

Answer 1

スライシングは、バリュー分析結果を使用するPDG（Program Dependent Graph）を計算する必要があります。 unreachable entry pointという警告は、あなたが与えた文脈で、関数fooに到達できない（つまり、到達不能ステートメントから呼び出された）ことを意味します。あなたが提供する出力に含まに

、ライン気づく：...たとえばなく、より

---

EDITをあなたに伝えるために

困難

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);です。入力コンテキストのデフォルト値はargvの場合は2です。これは、オプション-context-width 3を使用するか、または引数を取らない別のエントリポイントを使用して（-main my_mainで指定して）、argcとargvを明示的に定義して、mainと呼びます。

値の分析結果がOKであるかどうかを確認した後でのみ、スライシングを使用することをお勧めします。 -valオプションで単独で実行し、必要に応じて他のオプションを調整できます。