如何添加此getchar的規範以防止分段錯誤核心轉儲

我是Frama-c中的初學者。我在Value演示中找到了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: 
*/

來源

2017-06-05 user5784597

OCaml toplevel，版本4.02.3 gcc（Ubuntu 5.4.0-6ubuntu1〜16.04.4）5.4.0 20160609 linux是ubuntu 16.04我使用「gcc stub.c」編譯了這個程序，然後運行它「。 /a.out acf「，鍵入」c「，表示分段錯誤！謝謝 – user5784597

其實，_C_代碼崩潰了，而不是Frama-C。 – byako

我用錯誤的方式表達了 – user5784597

您getchar功能的正確規範可能是

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

這表示，由於參數的點提供一個有效的內存，其內容是由用戶提供的信息初始化的指針（在此處建模爲\nothing），並且該*p保證在執行getchar時被初始化。

當您使用Eva分析此程序時，您將獲得有關訪問string[idx]的警報。這是預期的，因爲你從未指定string確實是一個有效的C字符串。所以Frama-C/Eva確實檢測到這個代碼是不安全的。您可以要求string使用__fc_string_axiomatic.h的謂詞\valid_read_string有效。但是，警報將保留下來，因爲分析儀在分析中尚不夠智能，無法使用這些信息。

最後，你的代碼有很多問題。首先，main的正確原型是int main(int argc, char** argv)。 Frama-C並不在意，但gcc。其次，getchar的正確原型是int getchar(void)。如果您包含stdio.h，那麼您的代碼根本無法編譯。我實際上不確定a.out二進制文件在做什麼。

來源

2017-06-06 10:17:07 byako

感謝您耐心的解答，我重寫程序如下：

#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; 
}

起源計劃是從描述爲EVA教程的PDF的例子，但它的確爲GCC崩潰，而不是郵資-C @byako，我是frama-c和靜態代碼分析的初學者，並且學習如何爲程序編寫規範並證明它！再次感謝！

來源

2017-06-11 05:27:03 user5784597

如何添加此getchar的規範以防止分段錯誤核心轉儲

回答

相關問題