このgetcharの仕様を追加してセグメンテーションを回避する方法フォールト・コア・ダンプ

Question

私はFrama-cの初心者です。値プレゼンテーションにstub.cファイルが見つかりました。このプログラムの仕様を追加して境界を確認し、それを証明するにはどうすればよいですか？ありがとう。あなたのgetchar関数の

void getchar(char* p); 

int main(char* string) { 
    char c; 
    int idx = 0; 
    getchar(&c); 
    while(string[idx]) { 
      if (string[idx] == c) return idx; 
      idx++; 
    } 
    return -1; 
} 

/* 
Local Variables: 
compile-command: "frama-c -val stub.c" 
End: 
*/ 

Answer 1

正しい仕様は、おそらく

/*@ requires \valid(p); 
    assigns *p \from \nothing; 
    ensures \initialized(p); 
*/ 
void getchar(char* p); 

これは（その内容は、ユーザーが入力した情報から初期化されていることを、ポインタが有効なメモリへの引数のポイントとして供給することを表現していますここでは\nothingでモデル化されています）、getcharが実行された後に*pが初期化されることが保証されています。

Evaを使用してこのプログラムを分析すると、string[idx]へのアクセスに関する警告が表示されます。 stringが本当に有効なC文字列であることは決して指定されていないので、これは予想されます。そのため、Frama-C/Evaはこのコードが安全でないことを検出します。述語\valid_read_stringを__fc_string_axiomatic.hから有効にするには、stringを有効にする必要があります。しかし、アナライザは解析にこの情報を使用するほどスマートではないため、アラームは残っています。

最後に、コードにはかなりの問題があります。まず、mainの正しいプロトタイプはint main(int argc, char** argv)です。 Frama-Cは本当に気にしませんが、gccはありません。次に、getcharの正しいプロトタイプはint getchar(void)です。 stdio.hを含めると、コードはまったくコンパイルされません。私は実際にバイナリが何をしているのか分からない。

Answer 2

あなたの患者の答えのおかげで、私は以下のように、プログラムを書き換える：起点プログラムはEVAのためのチュートリアルを記述したPDFファイルからの例だった

#include <stdio.h> 
#include <string.h> 
#include "limits.h" 

int main() 
{ 
    char c; 
    char *str = "abgfc"; 
    int idx = 0; 
    c = getchar(); 
    int len = strlen(str); 

    /*@ requires \valid_read((char *)str + (0..idx)); 
    requires idx < INT_MAX; 
    behavior exists: 
     assumes \exists integer idx; str[idx] == c; 
    */ 

    /*@loop invariant 0 <= idx <= len; 
    loop assigns idx; 
    */ 
    while(str[idx]) 
    { 
     if(str[idx] == c) 
     { 
      return idx; 
     } 
     idx++; 
    } 
    return -1; 
} 

、それはFRAMA-C、gccのためにクラッシュをしませんでした@byako、私はframa-c ansスタティックコード解析の初心者で、プログラムの仕様を書いてそれを証明する方法を学びます！再度、感謝します！