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 : Sélectionner tout - Visualiser dans une fenêtre à part
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 : Sélectionner tout - Visualiser dans une fenêtre à part
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 : Sélectionner tout - Visualiser dans une fenêtre à part
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 ?