Analyseur code pour dépassement mémoire
Bonjour à tous,
j'utilise Splint pour analyser mon code C et je souhaite que le résultat de l'analyse me dise les failles de gestion mémoire du genre :
Code:
1
2
3
4
5
|
int *pointeur;
pointeur = malloc(10*sizeof(int));
pointeur[15] = 3;
free(pointeur); |
Comme on le sait, ce code passe à la compilation mais provoque des erreurs à l'exécution. C'est pourquoi le mieux est de le détecter avant.
Splint me dit bien qu'il y a une possibilité que pointeur soit NULL, là impécable, je suis d'accords, il faut donc ajouter un if(!NULL) avant d'utiliser le pointeur.
Mais ce que je veux c'est qu'il m'indique que la ligne pointeur[15] = 3; provoque un déppassement, comme il le fait si j'utilise des tableau :
Code:
1
2
3
|
int tableau[10];
tableau[15] = 3; |
dans cet exemple, Splint m'indique bien qu'il y a dépassement car 15 est plus grand que 10-1.
J'ai essayé avec des commandes Splint du genre
Code:
1
2
3
4
5
6
|
int *pointeur;
pointeur = malloc(10*sizeof(int));
/*@requires maxSet(pointeur) == 10-1@*/
pointeur[15] = 3;
free(pointeur); |
mais Splint ne semble pas comprendre ce que je lui dis.
Quelqu'un à t'il une idée de comment faire ?
Est-ce possible ?
Existe-t-il un analyseur statique qui sache le faire ?
