0
我有以下代碼片段。看似無效的內存訪問未被CMBC報告
#include<stdio.h>
#include<stdlib.h>
int main()
{
char *c = malloc(1);
printf("%p\n", c);
c = c + 20;
printf("%p\n", c);
printf("%d\n", *c);
free(c - 20);
return 0;
}
在這段代碼中，我將一個字節的內存分配給一個指針。然後，我正在訪問一個分配了內存20個單元的內存位置。當我解除引用指針時，我預計會得到內存訪問衝突錯誤或分段錯誤或類似的東西。我沒有得到任何這樣的錯誤。
讓我們假設這是一個未定義的行爲的情況。所以我試圖用CBMC這個衆所周知的模型檢查器使用下面的命令來驗證這個程序。
cbmc test01.c --pointer-check
CBMC報告說程序是安全的。這是CBMC的問題還是我錯過了什麼？
看到'g ++'with -'fsanitize = address'說了這個很有趣。我看不出任何方式，這將是「好」;也許這是一個CBMC錯誤？ – OMGtechy
如果訪問仍在堆分配內，則不會收到內存訪問衝突。 C沒有用數組索引來握住你的手。 –
'我期望得到一個內存訪問衝突錯誤。我沒有得到那個錯誤。「是什麼讓你覺得'c + 20'有受保護的內存？使用'（void *）c'代替'％p' –