Hat der GCC-Compiler eine Option, um die Speicherbeschädigung während der Kompilierung zu erkennen?

Question

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

int main() 
{ 
    char arrDst[5] = {0}; 
    char arrSrc[10] = "123456"; 
    memcpy(arrDst, arrSrc, sizeof(arrSrc)); 
    return 0; 
} 

Hier in diesem Programm ist es klar, dass es eine Speicherbeschädigung gibt.

Gibt es eine Option im GCC-Compiler, mit der ich dieses Problem zur Kompilierzeit erkennen kann?

Hinweis: Ich verwendete valgrind --leak-check=full, aber es hilft nicht.

Answer 1

$ gcc -Wall -O1 t.c 
In file included from /usr/include/string.h:642:0, 
       from t.c:3: 
In function ‘memcpy’, 
    inlined from ‘main’ at t.c:13:9: 
/usr/include/bits/string3.h:52:3: warning: call to __builtin___memcpy_chk 
    will always overflow destination buffer [enabled by default] 

GCC können einige davon erkennen. Das erfordert in der Regel das Aktivieren von Optimierungen (mindestens -01) und Warnungen (-Wall, fügen Sie auch -Wextra hinzu).

Answer 2

Es ist nicht zum großen Programm skalieren können Sie wirklich daran interessiert sind, aber Sie können diesen Fehler mit Frama-C finden:

$ frama-c -cpp-command "gcc -C -E -I`frama-c -print-share-path`/libc/ -nostdinc" mem.c `frama-c -print-share-path`/libc/fc_runtime.c -val 
... 
[value] computing for function memcpy <- main. 
    Called from mem.c:13. 
.../libc/string.h:54:[value] Function memcpy: precondition got status invalid. 

Diese Meldung bedeutet, dass Sie memcpy() mit Argumenten aufrufen, die den Vertrag nicht erfüllen . In diesem Fall ist die Vorbedingung, die fehlschlägt, die erste in der Liste, die Gültigkeit des Ziels zum Schreiben:

/*@ requires \valid(((char*)dest)+(0..n - 1));                             
    @ requires \valid_read(((char*)src)+(0..n - 1));                            
    @ requires \separated(((char *)dest)+(0..n-1),((char *)src)+(0..n-1));                       
    @ assigns ((char*)dest)[0..n - 1] \from ((char*)src)[0..n-1];                         
    @ assigns \result \from dest;                                 
    @ ensures memcmp((char*)dest,(char*)src,n) == 0;                            
    @ ensures \result == dest;                                  
    @*/ 
extern void *memcpy(void *restrict dest, 
        const void *restrict src, size_t n);