Frama-cでCコードをスライス

Question

私はframa-cで示されている未使用の変数をスライスしたいと思います。しかし、私はラインコマンドは考えが、私はhttps://frama-c.com/slicing.htmlに述べたように、1つのコマンドライン

Last login: Thu Nov 9 20:48:42 on ttys000 
Recep-MacBook-Pro:~ recepinanir$ cd desktop 
Recep-MacBook-Pro:desktop recepinanir$ cat hw.c 
#include <stdio.h> 

int main() 
{ 
    int x= 10; 
    int y= 24; 
    int z; 

    printf("Hello World\n"); 

    return 0; 
} 

Recep-MacBook-Pro:desktop recepinanir$ clang hw.c 
Recep-MacBook-Pro:desktop recepinanir$ ./a.out 
Hello World 
Recep-MacBook-Pro:desktop recepinanir$ clang -Wall hw.c -o result 
hw.c:5:9: warning: unused variable 'x' [-Wunused-variable] 
    int x= 10; 
     ^
hw.c:6:9: warning: unused variable 'y' [-Wunused-variable] 
    int y= 24; 
     ^
hw.c:7:9: warning: unused variable 'z' [-Wunused-variable] 
    int z; 
     ^
3 warnings generated. 
Recep-MacBook-Pro:desktop recepinanir$ 

Answer 1

を持つすべての未使用の変数をスライスするために書くべきではありません持って、スライスは常に相対的ないくつかの基準である、との目標は、小さいプログラムを作成することです元のものに戻し、基準に関して同じ振舞いを提示する。スライシングプラグイン自体は、そのような基準を作成するいくつかの方法を示していますが、Sparecodeプラグイン（https://frama-c.com/sparecode.html）の結果に興味があるようです。これは、スライスの特殊バージョンです。ここで、基準は最後のプログラム状態ですあなたの分析のエントリーポイント（あなたのケースではmain）を入力してください。言い換えれば、Sparecodeは分析中のコードの最終結果に寄与しないすべてのものを削除します。あなたのケースでは、frama-c -sparecode-analysis hw.cは次の結果を与えます（printfへの呼び出しはVariadicプラグインによって変更されており、その引数はmainの最終状態にとって有益ではないと考えられます）これ：一般的な場合では、スライス（従ってSparecode）はoverapproximationを与えることに注意し、最後

/* Generated by Frama-C */ 
#include "stdio.h" 
/*@ assigns \result, __fc_stdout->__fc_FILE_data; 
    assigns \result 
     \from (indirect: __fc_stdout->__fc_FILE_id), 
      __fc_stdout->__fc_FILE_data; 
    assigns __fc_stdout->__fc_FILE_data 
     \from (indirect: __fc_stdout->__fc_FILE_id), 
      __fc_stdout->__fc_FILE_data; 
*/ 
int printf_va_1(void); 

int main(void) 
{ 
    int __retres; 
    printf_va_1(); 
__retres = 0; 
return __retres; 
} 

）は、いくつかのグローバル変数に影響を与えることを示すACSL仕様に、より専門的な出力機能を提供するために必要dは彼らが基準に影響を与えないことが確実である陳述を削除するだけです。